From e2da03c11fa37f82d24f3a11c93aca7537a97f6a Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 15 Jun 2018 15:11:13 +0100
Subject: 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.
---
 lib/arith.sail | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib/arith.sail')

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
 
-- 
cgit v1.2.3