test/c/assign_rename_bug.sail


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
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
}