From c81f2fbdeef670e8cbd6771ecd22ce1e64f2306b Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 2 Mar 2020 18:20:02 +0000
Subject: Add arith_shiftr to SMT and interpreter

---
 src/value.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/value.ml')

diff --git a/src/value.ml b/src/value.ml
index f94ae176..11cda94b 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -457,6 +457,10 @@ let value_shiftr = function
   | [v1; v2] -> mk_vector (Sail_lib.shiftr (coerce_bv v1, coerce_int v2))
   | _ -> failwith "value shiftr"
 
+let value_arith_shiftr = function
+  | [v1; v2] -> mk_vector (Sail_lib.arith_shiftr (coerce_bv v1, coerce_int v2))
+  | _ -> failwith "value arith_shiftr"
+
 let value_shift_bits_left = function
   | [v1; v2] -> mk_vector (Sail_lib.shift_bits_left (coerce_bv v1, coerce_bv v2))
   | _ -> failwith "value shift_bits_left"
@@ -697,6 +701,7 @@ let primops = ref
        ("ones", value_ones);
        ("shiftr", value_shiftr);
        ("shiftl", value_shiftl);
+       ("arith_shiftr", value_shiftr);
        ("shift_bits_left", value_shift_bits_left);
        ("shift_bits_right", value_shift_bits_right);
        ("add_int", value_add_int);
-- 
cgit v1.2.3