From fffcaaa390eaf03db689d0f108cc00653a41885d Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 10 May 2017 16:10:28 +0100
Subject: 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.
---
 cheri/cheri_insts.sail | 4 ++--
 1 file 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 *)
 }
 
-- 
cgit v1.2.3