diff options
| author | Robert Norton | 2017-04-20 11:54:16 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-04-20 11:54:16 +0100 |
| commit | ae711f2bb22410667d14788fc9451cc8aba65399 (patch) | |
| tree | 67ad5f3ed43816277a6065dadabfb7a526ec2a0e /cheri | |
| parent | c8d5abad7f46df85ec6e1d47c28454077354c066 (diff) | |
work around ocaml shallow embedding problem with matching on big_ints by restructuing switch as if
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index 45acd949..4c6ca486 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -230,11 +230,12 @@ function bool fastRepCheck((CapStruct) c, (bit[64]) i) = (2**(E+20)) and 2. whether it is positive or negative. To satisfy 1. all top bits must be the same so we are interested in the cases i_top is 0 or -1 *) - switch(i_top) { - case 0 -> i_mid <_u diff1 - case -1 -> unsigned(i_mid) >= unsigned(diff) & (R != a_mid) (* XXX sail missing unsigned >= *) - case _ -> false - } + if (i_top == 0) then + i_mid <_u diff1 + else if (i_top == -1) then + unsigned(i_mid) >= unsigned(diff) & (R != a_mid) (* XXX sail missing unsigned >= *) + else + false function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = let (bit[64]) base = (bit[64]) (getCapBase(c)) in |