diff options
| author | Alasdair Armstrong | 2018-06-15 15:11:13 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-06-15 15:12:24 +0100 |
| commit | e2da03c11fa37f82d24f3a11c93aca7537a97f6a (patch) | |
| tree | a43a199ee2b448f7c970dc155ae8bc88fac8fe49 /lib/arith.sail | |
| parent | 5dc3ee5029f6e828b7e77a176a67894e8fa00696 (diff) | |
Fixes for C RTS for aarch64 no it's split into multiple files
Fix a bug involving indentifers on the left hand side of assignment
statements not being shadowed correctly within foreach loops.
Make the different between different types of integer division
explicit in at least the C compilation for now. fdiv_int is division
rounding towards -infinity (floor). while tdiv_int is truncating
towards zero. Same for fmod_int and tmod_int.
Diffstat (limited to 'lib/arith.sail')
| -rw-r--r-- | lib/arith.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index f713805a..e5d2d6ea 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -54,7 +54,7 @@ val div_int = { smt: "div", ocaml: "quotient", lem: "integerDiv", - c: "div_int", + c: "tdiv_int", coq: "Z.quot" } : (int, int) -> int @@ -64,7 +64,7 @@ val mod_int = { smt: "mod", ocaml: "modulus", lem: "integerMod", - c: "mod_int", + c: "tmod_int", coq: "Z.rem" } : (int, int) -> int |