diff options
Diffstat (limited to 'test/c')
| -rw-r--r-- | test/c/assign_rename_bug.expect | 28 | ||||
| -rw-r--r-- | test/c/assign_rename_bug.sail | 35 |
2 files changed, 63 insertions, 0 deletions
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 +} |
