diff options
| -rw-r--r-- | cheri/cheri_insts.sail | 4 | ||||
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 2 |
2 files changed, 1 insertions, 5 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index c832d70c..92c56cc4 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -795,8 +795,6 @@ function clause execute (CCheckPerm(cs, rt)) = raise_c2_exception(CapEx_TagViolation, cs) else if ((cs_perms & rt_perms) != rt_perms) then raise_c2_exception(CapEx_UserDefViolation, cs) - else - () /* END_CCheckPerm */ } @@ -821,8 +819,6 @@ function clause execute (CCheckType(cs, cb)) = raise_c2_exception(CapEx_SealViolation, cb) else if ((cs_val.otype) != (cb_val.otype)) then raise_c2_exception(CapEx_TypeViolation, cs) - else - () /* END_CCheckType */ } diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index 9f91ae77..d1129147 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -302,7 +302,7 @@ function incCapOffset(c, delta) : (CapStruct, bits(64)) -> (bool, CapStruct) = val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, 0 <= 'n < 'N . option(atom('n))} function HighestSetBit x = { foreach (i from ('N - 1) to 0 by 1 in dec) - if [x[i]] == 0b1 then return Some(i) else (); + if [x[i]] == 0b1 then return Some(i); return None() : option(atom(0)) } |