summaryrefslogtreecommitdiff
path: root/lib/arith.sail
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-01-29 19:24:11 +0000
committerAlasdair Armstrong2019-01-29 19:24:35 +0000
commitcca2016b7a339da00fcf8ffdf8e5e758234a0234 (patch)
treeb980efb937a206b01270fe4d029138551d08003a /lib/arith.sail
parent36fd3c158c08af5b48d9801a607f3be812d2ecc7 (diff)
Fixes for full v8.5
Diffstat (limited to 'lib/arith.sail')
-rw-r--r--lib/arith.sail6
1 files changed, 5 insertions, 1 deletions
diff --git a/lib/arith.sail b/lib/arith.sail
index a3a80fc5..b233048e 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -70,7 +70,11 @@ val _shl_int = "shl_int" : (int, int) -> int
overload shl_int = {_shl8, _shl32, _shl_int}
-val shr_int = "shr_int" : (int, int) -> int
+val _shr32 = {c: "shr_mach_int", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)}
+
+val _shr_int = "shr_int" : (int, int) -> int
+
+overload shr_int = {_shr32, _shr_int}
// ***** div and mod *****