diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 92ef7037..50dacf5e 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -69,12 +69,11 @@ let rec replace bs (n : integer) b' = match bs with let upper n = n +(* Modulus operation corresponding to quot below -- result + has sign of dividend. *) let hardware_mod (a: integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) mod (abs b) - else if (a < 0 && b >= 0) - then (a mod b) - b - else a mod b + let m = (abs a) mod (abs b) in + if a < 0 then ~m else m (* There are different possible answers for integer divide regarding rounding behaviour on negative operands. Positive operands always |