summaryrefslogtreecommitdiff
path: root/cheri
diff options
context:
space:
mode:
Diffstat (limited to 'cheri')
-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 4b61318d..e9414547 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -407,6 +407,8 @@ function clause execute (CCheckPerm(cs, rt)) =
exit (raise_c2_exception(CapEx_TagViolation, cs))
else if ((cs_perms & rt_perms) != rt_perms) then
exit (raise_c2_exception(CapEx_UserDefViolation, cs))
+ else
+ ()
(* END_CCheckPerm *)
}