diff options
| -rw-r--r-- | lib/arith.sail | 4 | ||||
| -rw-r--r-- | src/value.ml | 5 |
2 files changed, 7 insertions, 2 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 8825ac2f..20231de1 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -94,7 +94,7 @@ val mod_int = { lem: "integerMod", c: "tmod_int", coq: "Z.rem" -} : (int, int) -> int +} : (int, int) -> nat overload operator % = {mod_int} @@ -104,6 +104,6 @@ val abs_int = { lem: "abs_int", c: "abs_int", coq: "Z.abs" -} : (int, int) -> int +} : int -> int $endif diff --git a/src/value.ml b/src/value.ml index 729b3974..8f8e651a 100644 --- a/src/value.ml +++ b/src/value.ml @@ -331,6 +331,10 @@ let value_modulus = function | [v1; v2] -> V_int (Sail_lib.modulus (coerce_int v1, coerce_int v2)) | _ -> failwith "value modulus" +let value_abs_int = function + | [v] -> V_int (Big_int.abs (coerce_int v)) + | _ -> failwith "value abs_int" + let value_add_vec_int = function | [v1; v2] -> mk_vector (Sail_lib.add_vec_int (coerce_bv v1, coerce_int v2)) | _ -> failwith "value add_vec_int" @@ -630,6 +634,7 @@ let primops = ("shl_int", value_shl_int); ("max_int", value_max_int); ("min_int", value_min_int); + ("abs_int", value_abs_int); ("add_vec_int", value_add_vec_int); ("sub_vec_int", value_sub_vec_int); ("add_vec", value_add_vec); |