[Header]

open Program
open D
open Unix

let stdin_redirect_f = "stdin_redirect.txt"
  
let analyze pgm_str input_str =
  let pgm = Parser.program Lexer.start (Lexing.from_string pgm_str) in
  (* Write testcase input string to a file *)
  let chan = open_out stdin_redirect_f in
  let _ = Printf.fprintf chan input_str in
  let _ = close_out chan in
  (* Stdin Redirection *)
  let new_stdin = open_in stdin_redirect_f in
  let _ = Unix.dup2 (Unix.descr_of_in_channel new_stdin) Unix.stdin in
  let result = D.dintp pgm in
  D.string_of_mem result

[Test]
analyze 
"
x := 2;
y := 3;
z := -((x + y) * 5)
"

""

[Value]
"[x |-> 2 ; y |-> 3 ; z |-> -25]"

[Test]
analyze 
"
x := 2;
y := 3;
(if ( x < 1 )
  then r := 5
  else (
    r := 3; 
    (if ( 2 < y )
      then r := (r + 4)
      else r := (r + 9)
    )
  )
)
"

""

[Value]
"[r |-> 7 ; x |-> 2 ; y |-> 3]"

[Test]
analyze 
"
x := 5;
y := 4;
z := 3;
while (0 < x) do (
    x := x + (- 1);
    y := y + 1;
    (if (6 < y)
      then z := z * 2
      else z := z + (- 1))
)
"

""

[Value]
"[x |-> 0 ; y |-> 9 ; z |-> 8]"

[Test]
analyze 
"
x := 5;
y := 2;
(if (10 < x)
  then goto 12
  else goto 9);
x := x + (y + 1);
goto 2;
y := 100
"

""

[Value]
"[x |-> 11 ; y |-> 100]"

[Test]
analyze 
"
x := 2;
y := 3;
z := &y;
y := y + 1;
x := *z + 1;
*z := 1
"

""

[Value]
"[x |-> 5 ; y |-> 1 ; z |-> y]"

[Test]
analyze 
"
w := 2;
x := read;
w := read;
x := 1;
y := read;
z := (w + (-y)) * 5
"

"3\n4\n5\n"

[Value]
"[w |-> 4 ; x |-> 1 ; y |-> 5 ; z |-> -5]"

[Test]
analyze 
"
x := 2;
y := 4;
z := 3;
while ((-1) < x) do (
    x := x + (- 1);
    y := y + 1;
    (if (z < 5)
      then goto 20
      else goto 23
    )
);
(if ((- 1) < x)
  then goto 7
  else x := (- 1));
z := z + 1;
goto 15;
z := 0
"

""

[Value]
"[x |-> -1 ; y |-> 7 ; z |-> 0]"

[Test]
analyze 
"
x := 5;
y := 4;
z := 3;
w := &z;
while (0 < x) do (
    x := x + (- 1);
    y := y + 1;
    (if (6 < y)
      then *w := z * 2
      else z := *w + (- 1))
)
"

""

[Value]
"[w |-> z ; x |-> 0 ; y |-> 9 ; z |-> 8]"

[Test]
analyze 
"
x := 2;
y := 3;
z := &y;
w := &z;
y := y + 1;
x := *z + 1;
*z := *z + 2
"

""

[Value]
"[w |-> z ; x |-> 5 ; y |-> 6 ; z |-> y]"


[Test]
analyze 
"
w := read;
x := 2;
y := 4;
z := 3;
v := &x;
while ((-1) < x) do (
    x := *v + (- 1);
    y := y + 1;
    (if (z < 5)
      then goto 24
      else goto 29
    )
);
(if ((- 1) < *v)
  then goto 11
  else x := (- 1));
z := z + 1;
w := *v * w;
goto 20;
z := 0
"

"123\n"

[Value]
"[v |-> x ; w |-> 0 ; x |-> -1 ; y |-> 7 ; z |-> 0]"