From cca2016b7a339da00fcf8ffdf8e5e758234a0234 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 29 Jan 2019 19:24:11 +0000
Subject: Fixes for full v8.5

---
 lib/arith.sail | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'lib/arith.sail')

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 *****
 
-- 
cgit v1.2.3


From 55f65f92812a6927d5661c2c25a09051630334b3 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 6 Feb 2019 15:26:32 +0000
Subject: Fix some tests

---
 lib/arith.sail | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib/arith.sail')

diff --git a/lib/arith.sail b/lib/arith.sail
index b233048e..8825ac2f 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -102,6 +102,7 @@ val abs_int = {
   smt : "abs",
   ocaml: "abs_int",
   lem: "abs_int",
+  c: "abs_int",
   coq: "Z.abs"
 } : (int, int) -> int
 
-- 
cgit v1.2.3