summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThomas Bauereiss2017-05-10 16:10:28 +0100
committerThomas Bauereiss2017-05-10 16:10:28 +0100
commitfffcaaa390eaf03db689d0f108cc00653a41885d (patch)
treef62ac8e64857715459b68dcd7891296b170ce71e
parent5984dca66a9a5f25077b8451796f08639479b489 (diff)
Fix type error in CGetLen
For some reason, Lem did not like the call to "min" when exporting to Isabelle. Replacing "min" with an if-then-else expression solves this. This is also in line with the CHERI spec, which actually uses an if block.
-rw-r--r--cheri/cheri_insts.sail4
1 files changed, 2 insertions, 2 deletions
diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index b2801bae..b11dadfa 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -108,8 +108,8 @@ function clause execute (CGetLen(rd, cb)) =
else
let capVal = readCapReg(cb) in
let len65 = getCapLength(capVal) in
- let len64 = (bit[64]) (min(MAX_U64, len65)) in
- wGPR(rd) := len64;
+ let len64 = (if len65 > MAX_U64 then MAX_U64 else len65) in
+ wGPR(rd) := (bit[64]) len64;
(* END_CGetLen *)
}