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.
---
 test/c/assign_rename_bug.expect | 28 ++++++++++++++++++++++++++++
 test/c/assign_rename_bug.sail   | 35 +++++++++++++++++++++++++++++++++++
 2 files changed, 63 insertions(+)
 create mode 100644 test/c/assign_rename_bug.expect
 create mode 100644 test/c/assign_rename_bug.sail

(limited to 'test')

diff --git a/test/c/assign_rename_bug.expect b/test/c/assign_rename_bug.expect
new file mode 100644
index 00000000..ef2503c0
--- /dev/null
+++ b/test/c/assign_rename_bug.expect
@@ -0,0 +1,28 @@
+0xFFF0000000001
+0xFFF0000000001
+0xFFEFFFFFFFFFF
+0xFFEFFFFFFFFFF
+0xFFF0000000002
+0xFFF0000000002
+0xFFEFFFFFFFFFE
+0xFFEFFFFFFFFFE
+0xFFF0000000003
+0xFFF0000000003
+0xFFEFFFFFFFFFD
+0xFFEFFFFFFFFFD
+0xFFF0000000004
+0xFFF0000000004
+0xFFEFFFFFFFFFC
+0xFFEFFFFFFFFFC
+0xFFF0000000005
+0xFFF0000000005
+0xFFEFFFFFFFFFB
+0xFFEFFFFFFFFFB
+0xFFF0000000006
+0xFFF0000000006
+0xFFEFFFFFFFFFA
+0xFFEFFFFFFFFFA
+0xFFF0000000007
+0xFFF0000000007
+0xFFEFFFFFFFFF9
+0xFFEFFFFFFFFF9
diff --git a/test/c/assign_rename_bug.sail b/test/c/assign_rename_bug.sail
new file mode 100644
index 00000000..8b74df2a
--- /dev/null
+++ b/test/c/assign_rename_bug.sail
@@ -0,0 +1,35 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+$include <vector_dec.sail>
+
+$include <exception_basic.sail>
+
+val sub_vec_int = {
+  ocaml: "sub_vec_int",
+  lem: "sub_vec_int",
+  c: "sub_bits_int"
+} : forall 'n. (bits('n), int) -> bits('n)
+
+overload operator - = {sub_vec_int}
+
+val print_bits52: (string, bits(52)) -> unit
+
+function print_bits52(str, x) = print_bits(str, x)
+
+val main : unit -> unit effect {undef}
+
+function main() = {
+  let addr : bits(52) = 0xF_FF00_0000_0000;
+  i : int = undefined;
+  size : int = 7;
+  ret : unit = ();
+  foreach (i from 1 to size by 1 in inc) {
+    ret = print_bits("", addr + i);
+    ret = print_bits52("", addr + i);
+    ret = print_bits("", addr - i);
+    ret = print_bits52("", addr - i);
+  };
+  return ret
+}
-- 
cgit v1.2.3