summaryrefslogtreecommitdiff
path: root/src/value.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2020-02-06 17:20:39 +0000
committerAlasdair Armstrong2020-02-06 17:21:20 +0000
commit4a72cb8084237161d0bccc66f27d5fb6d24315e0 (patch)
tree04b824a9190795185a24c7c2679c60dd03592d43 /src/value.ml
parentda1309632d35c910a6d3ae14ad2f5af037fce89e (diff)
Make sure tdiv_int and tmod_int are recognised by sail -i
Diffstat (limited to 'src/value.ml')
-rw-r--r--src/value.ml10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/value.ml b/src/value.ml
index 69023bc3..3a9a071f 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -369,6 +369,14 @@ let value_mult = function
| [v1; v2] -> V_int (Sail_lib.mult (coerce_int v1, coerce_int v2))
| _ -> failwith "value mult"
+let value_tdiv_int = function
+ | [v1; v2] -> V_int (Sail_lib.tdiv_int (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value tdiv_int"
+
+let value_tmod_int = function
+ | [v1; v2] -> V_int (Sail_lib.tmod_int (coerce_int v1, coerce_int v2))
+ | _ -> failwith "value tmod_int"
+
let value_quotient = function
| [v1; v2] -> V_int (Sail_lib.quotient (coerce_int v1, coerce_int v2))
| _ -> failwith "value quotient"
@@ -687,6 +695,8 @@ let primops = ref
("sub_int", value_sub_int);
("sub_nat", value_sub_nat);
("div_int", value_quotient);
+ ("tdiv_int", value_tdiv_int);
+ ("tmod_int", value_tmod_int);
("mult_int", value_mult);
("mult", value_mult);
("quotient", value_quotient);