summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--cheri/cheri_insts.sail2
1 files changed, 2 insertions, 0 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index b4b28c01..b084faa0 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -434,6 +434,8 @@ function clause execute (CCheckType(cs, cb)) =
exit (raise_c2_exception(CapEx_SealViolation, cb))
else if ((cs_val.otype) != (cb_val.otype)) then
exit (raise_c2_exception(CapEx_TypeViolation, cs))
+ else
+ ()
(* END_CCheckType *)
}