summaryrefslogtreecommitdiff
path: root/cheri
diff options
context:
space:
mode:
authorRobert Norton2018-03-21 14:38:50 +0000
committerRobert Norton2018-03-27 15:57:38 +0100
commit8ada249efc7ae202c4a70af396ce5c771acd3de4 (patch)
tree1af02ab34f2ebceb11ec4146c17c3ed714f41675 /cheri
parentdf43534680d713c4671f3d24fb4713b1fbbcfb74 (diff)
remove some unneeded else clauses.
Diffstat (limited to 'cheri')
-rw-r--r--cheri/cheri_insts.sail4
-rw-r--r--cheri/cheri_prelude_128.sail2
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))
}