diff options
| author | Jon French | 2019-03-04 14:23:55 +0000 |
|---|---|---|
| committer | Jon French | 2019-03-04 14:23:55 +0000 |
| commit | 94d40fb68bb3d36159a006b93909fc3841c92d28 (patch) | |
| tree | 219c6d0ae7daf47cd6c8897895d182916e8f3815 /src/value.ml | |
| parent | a7a3402ce155f13234d2d3e5198e5dbf6e0e8b82 (diff) | |
| parent | 9ed89583d52ccff151fb75424975f2ac4e627a1b (diff) | |
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src/value.ml')
| -rw-r--r-- | src/value.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/value.ml b/src/value.ml index 261b0f4e..843a943b 100644 --- a/src/value.ml +++ b/src/value.ml @@ -343,6 +343,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" @@ -668,6 +672,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); |
