diff options
| author | Alasdair Armstrong | 2017-11-28 18:48:19 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-28 18:48:19 +0000 |
| commit | 0952ebb7800fe1c396f6916c33bbc19a3b895308 (patch) | |
| tree | a63a33c0f1503ab2eda44db2e7c54a8f7d9e4b8d /lib | |
| parent | 32a659a025cb239a32e8a831200e458af3c54c52 (diff) | |
Small update to trivial sizeof rewrites so we can handle all cases in
aarch64 vector instructions.
There's maybe a better more general way to do this but I'm not sure
what that would be.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/ocaml_rts/sail_lib.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml index 3cf4505d..dfdd1db9 100644 --- a/lib/ocaml_rts/sail_lib.ml +++ b/lib/ocaml_rts/sail_lib.ml @@ -413,6 +413,8 @@ let real_power (x, y) = Num.power_num x (Num.num_of_big_int y) let add_real (x, y) = Num.add_num x y let sub_real (x, y) = Num.sub_num x y +let abs_real x = Num.abs_num x + let lt (x, y) = lt_big_int x y let gt (x, y) = gt_big_int x y let lteq (x, y) = le_big_int x y @@ -422,6 +424,7 @@ let pow2 x = power_big_int_positive_int x 2 let max_int (x, y) = max_big_int x y let min_int (x, y) = min_big_int x y +let abs_int x = abs_big_int x let undefined_real () = Num.num_of_int 0 |
