[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.dcintp pgm) in
  D.string_of_col result

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

""

[Value]
"0:
{
 []
}
1:
{
 []
}
2:
{
 [x |-> 2]
}
3:
{
 [x |-> 2]
}
4:
{
 [x |-> 2 ; y |-> 3]
}
"
[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]
"0:
{
 []
}
1:
{
 []
}
2:
{
 [x |-> 2]
}
3:
{
 [x |-> 2]
}
4:
{
 [x |-> 2 ; y |-> 3]
}
5:
{}
6:
{
 [x |-> 2 ; y |-> 3]
}
7:
{
 [x |-> 2 ; y |-> 3]
}
8:
{
 [r |-> 3 ; x |-> 2 ; y |-> 3]
}
9:
{
 [r |-> 3 ; x |-> 2 ; y |-> 3]
}
10:
{}
"

[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]
"0:
{
 []
}
1:
{
 []
}
2:
{
 [x |-> 5]
}
3:
{
 [x |-> 5]
}
4:
{
 [x |-> 5 ; y |-> 4]
}
5:
{
 [x |-> 5 ; y |-> 4]
}
6:
{
 [x |-> 0 ; y |-> 9 ; z |-> 8],
 [x |-> 1 ; y |-> 8 ; z |-> 4],
 [x |-> 2 ; y |-> 7 ; z |-> 2],
 [x |-> 3 ; y |-> 6 ; z |-> 1],
 [x |-> 4 ; y |-> 5 ; z |-> 2],
 [x |-> 5 ; y |-> 4 ; z |-> 3]
}
7:
{
 [x |-> 1 ; y |-> 8 ; z |-> 4],
 [x |-> 2 ; y |-> 7 ; z |-> 2],
 [x |-> 3 ; y |-> 6 ; z |-> 1],
 [x |-> 4 ; y |-> 5 ; z |-> 2],
 [x |-> 5 ; y |-> 4 ; z |-> 3]
}
8:
{
 [x |-> 1 ; y |-> 8 ; z |-> 4],
 [x |-> 2 ; y |-> 7 ; z |-> 2],
 [x |-> 3 ; y |-> 6 ; z |-> 1],
 [x |-> 4 ; y |-> 5 ; z |-> 2],
 [x |-> 5 ; y |-> 4 ; z |-> 3]
}
9:
{
 [x |-> 0 ; y |-> 8 ; z |-> 4],
 [x |-> 1 ; y |-> 7 ; z |-> 2],
 [x |-> 2 ; y |-> 6 ; z |-> 1],
 [x |-> 3 ; y |-> 5 ; z |-> 2],
 [x |-> 4 ; y |-> 4 ; z |-> 3]
}
10:
{
 [x |-> 0 ; y |-> 8 ; z |-> 4],
 [x |-> 1 ; y |-> 7 ; z |-> 2],
 [x |-> 2 ; y |-> 6 ; z |-> 1],
 [x |-> 3 ; y |-> 5 ; z |-> 2],
 [x |-> 4 ; y |-> 4 ; z |-> 3]
}
11:
{
 [x |-> 0 ; y |-> 9 ; z |-> 4],
 [x |-> 1 ; y |-> 8 ; z |-> 2],
 [x |-> 2 ; y |-> 7 ; z |-> 1],
 [x |-> 3 ; y |-> 6 ; z |-> 2],
 [x |-> 4 ; y |-> 5 ; z |-> 3]
}
12:
{
 [x |-> 0 ; y |-> 9 ; z |-> 4],
 [x |-> 1 ; y |-> 8 ; z |-> 2],
 [x |-> 2 ; y |-> 7 ; z |-> 1]
}
13:
{
 [x |-> 3 ; y |-> 6 ; z |-> 2],
 [x |-> 4 ; y |-> 5 ; z |-> 3]
}
"

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

""

[Value]
"0:
{
 []
}
1:
{
 []
}
2:
{
 [x |-> 5],
 [x |-> 8 ; y |-> 2],
 [x |-> 11 ; y |-> 2]
}
3:
{
 [x |-> 5],
 [x |-> 8 ; y |-> 2],
 [x |-> 11 ; y |-> 2]
}
4:
{
 [x |-> 5 ; y |-> 2],
 [x |-> 8 ; y |-> 2],
 [x |-> 11 ; y |-> 2]
}
5:
{
 [x |-> 5 ; y |-> 2],
 [x |-> 8 ; y |-> 2],
 [x |-> 11 ; y |-> 2]
}
6:
{
 [x |-> 11 ; y |-> 2]
}
7:
{
 [x |-> 5 ; y |-> 2],
 [x |-> 8 ; y |-> 2]
}
8:
{}
9:
{
 [x |-> 5 ; y |-> 2],
 [x |-> 8 ; y |-> 2]
}
10:
{
 [x |-> 8 ; y |-> 2],
 [x |-> 11 ; y |-> 2]
}
11:
{
 [x |-> 8 ; y |-> 2],
 [x |-> 11 ; y |-> 2]
}
12:
{
 [x |-> 11 ; y |-> 2]
}
"

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

""

[Value]
"0:
{
 []
}
1:
{
 []
}
2:
{
 [x |-> 2]
}
3:
{
 [x |-> 2]
}
4:
{
 [x |-> 2 ; y |-> 3]
}
5:
{
 [x |-> 2 ; y |-> 3]
}
6:
{
 [x |-> 2 ; y |-> 3 ; z |-> y]
}
7:
{
 [x |-> 2 ; y |-> 3 ; z |-> y]
}
8:
{
 [x |-> 2 ; y |-> 4 ; z |-> y]
}
9:
{
 [x |-> 2 ; y |-> 4 ; z |-> y]
}
10:
{
 [x |-> 5 ; y |-> 4 ; z |-> y]
}
"

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

"3\n4\n5\n"

[Value]
"0:
{
 []
}
1:
{
 []
}
2:
{
 [w |-> 2]
}
3:
{
 [w |-> 2]
}
4:
{
 [w |-> 2 ; x |-> 3]
}
5:
{
 [w |-> 2 ; x |-> 3]
}
6:
{
 [w |-> 4 ; x |-> 3]
}
7:
{
 [w |-> 4 ; x |-> 3]
}
8:
{
 [w |-> 4 ; x |-> 1]
}
9:
{
 [w |-> 4 ; x |-> 1]
}
10:
{
 [w |-> 4 ; x |-> 1 ; y |-> 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]
"0:
{
 []
}
1:
{
 []
}
2:
{
 [x |-> 2]
}
3:
{
 [x |-> 2]
}
4:
{
 [x |-> 2 ; y |-> 4]
}
5:
{
 [x |-> 2 ; y |-> 4]
}
6:
{
 [x |-> 2 ; y |-> 4 ; z |-> 3]
}
7:
{
 [x |-> 0 ; y |-> 6 ; z |-> 5],
 [x |-> 1 ; y |-> 5 ; z |-> 4],
 [x |-> 2 ; y |-> 4 ; z |-> 3]
}
8:
{
 [x |-> 0 ; y |-> 6 ; z |-> 5],
 [x |-> 1 ; y |-> 5 ; z |-> 4],
 [x |-> 2 ; y |-> 4 ; z |-> 3]
}
9:
{
 [x |-> 0 ; y |-> 6 ; z |-> 5],
 [x |-> 1 ; y |-> 5 ; z |-> 4],
 [x |-> 2 ; y |-> 4 ; z |-> 3]
}
10:
{
 [x |-> -1 ; y |-> 6 ; z |-> 5],
 [x |-> 0 ; y |-> 5 ; z |-> 4],
 [x |-> 1 ; y |-> 4 ; z |-> 3]
}
11:
{
 [x |-> -1 ; y |-> 6 ; z |-> 5],
 [x |-> 0 ; y |-> 5 ; z |-> 4],
 [x |-> 1 ; y |-> 4 ; z |-> 3]
}
12:
{
 [x |-> -1 ; y |-> 7 ; z |-> 5],
 [x |-> 0 ; y |-> 6 ; z |-> 4],
 [x |-> 1 ; y |-> 5 ; z |-> 3]
}
13:
{
 [x |-> 0 ; y |-> 6 ; z |-> 4],
 [x |-> 1 ; y |-> 5 ; z |-> 3]
}
14:
{
 [x |-> -1 ; y |-> 7 ; z |-> 5]
}
15:
{
 [x |-> 0 ; y |-> 6 ; z |-> 5],
 [x |-> 1 ; y |-> 5 ; z |-> 4]
}
16:
{
 [x |-> 0 ; y |-> 6 ; z |-> 5],
 [x |-> 1 ; y |-> 5 ; z |-> 4]
}
17:
{
 [x |-> 0 ; y |-> 6 ; z |-> 5],
 [x |-> 1 ; y |-> 5 ; z |-> 4]
}
18:
{}
19:
{}
20:
{
 [x |-> 0 ; y |-> 6 ; z |-> 4],
 [x |-> 1 ; y |-> 5 ; z |-> 3]
}
21:
{
 [x |-> 0 ; y |-> 6 ; z |-> 5],
 [x |-> 1 ; y |-> 5 ; z |-> 4]
}
22:
{
 [x |-> 0 ; y |-> 6 ; z |-> 5],
 [x |-> 1 ; y |-> 5 ; z |-> 4]
}
23:
{
 [x |-> -1 ; y |-> 7 ; z |-> 5]
}
"

[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]
"0:
{
 []
}
1:
{
 []
}
2:
{
 [x |-> 5]
}
3:
{
 [x |-> 5]
}
4:
{
 [x |-> 5 ; y |-> 4]
}
5:
{
 [x |-> 5 ; y |-> 4]
}
6:
{
 [x |-> 5 ; y |-> 4 ; z |-> 3]
}
7:
{
 [x |-> 5 ; y |-> 4 ; z |-> 3]
}
8:
{
 [w |-> z ; x |-> 0 ; y |-> 9 ; z |-> 8],
 [w |-> z ; x |-> 1 ; y |-> 8 ; z |-> 4],
 [w |-> z ; x |-> 2 ; y |-> 7 ; z |-> 2],
 [w |-> z ; x |-> 3 ; y |-> 6 ; z |-> 1],
 [w |-> z ; x |-> 4 ; y |-> 5 ; z |-> 2],
 [w |-> z ; x |-> 5 ; y |-> 4 ; z |-> 3]
}
9:
{
 [w |-> z ; x |-> 1 ; y |-> 8 ; z |-> 4],
 [w |-> z ; x |-> 2 ; y |-> 7 ; z |-> 2],
 [w |-> z ; x |-> 3 ; y |-> 6 ; z |-> 1],
 [w |-> z ; x |-> 4 ; y |-> 5 ; z |-> 2],
 [w |-> z ; x |-> 5 ; y |-> 4 ; z |-> 3]
}
10:
{
 [w |-> z ; x |-> 1 ; y |-> 8 ; z |-> 4],
 [w |-> z ; x |-> 2 ; y |-> 7 ; z |-> 2],
 [w |-> z ; x |-> 3 ; y |-> 6 ; z |-> 1],
 [w |-> z ; x |-> 4 ; y |-> 5 ; z |-> 2],
 [w |-> z ; x |-> 5 ; y |-> 4 ; z |-> 3]
}
11:
{
 [w |-> z ; x |-> 0 ; y |-> 8 ; z |-> 4],
 [w |-> z ; x |-> 1 ; y |-> 7 ; z |-> 2],
 [w |-> z ; x |-> 2 ; y |-> 6 ; z |-> 1],
 [w |-> z ; x |-> 3 ; y |-> 5 ; z |-> 2],
 [w |-> z ; x |-> 4 ; y |-> 4 ; z |-> 3]
}
12:
{
 [w |-> z ; x |-> 0 ; y |-> 8 ; z |-> 4],
 [w |-> z ; x |-> 1 ; y |-> 7 ; z |-> 2],
 [w |-> z ; x |-> 2 ; y |-> 6 ; z |-> 1],
 [w |-> z ; x |-> 3 ; y |-> 5 ; z |-> 2],
 [w |-> z ; x |-> 4 ; y |-> 4 ; z |-> 3]
}
13:
{
 [w |-> z ; x |-> 0 ; y |-> 9 ; z |-> 4],
 [w |-> z ; x |-> 1 ; y |-> 8 ; z |-> 2],
 [w |-> z ; x |-> 2 ; y |-> 7 ; z |-> 1],
 [w |-> z ; x |-> 3 ; y |-> 6 ; z |-> 2],
 [w |-> z ; x |-> 4 ; y |-> 5 ; z |-> 3]
}
14:
{
 [w |-> z ; x |-> 0 ; y |-> 9 ; z |-> 4],
 [w |-> z ; x |-> 1 ; y |-> 8 ; z |-> 2],
 [w |-> z ; x |-> 2 ; y |-> 7 ; z |-> 1]
}
15:
{
 [w |-> z ; x |-> 3 ; y |-> 6 ; z |-> 2],
 [w |-> z ; x |-> 4 ; y |-> 5 ; z |-> 3]
}
"

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

""

[Value]
"0:
{
 []
}
1:
{
 []
}
2:
{
 [x |-> 2]
}
3:
{
 [x |-> 2]
}
4:
{
 [x |-> 2 ; y |-> 3]
}
5:
{
 [x |-> 2 ; y |-> 3]
}
6:
{
 [x |-> 2 ; y |-> 3 ; z |-> y]
}
7:
{
 [x |-> 2 ; y |-> 3 ; z |-> y]
}
8:
{
 [w |-> z ; x |-> 2 ; y |-> 3 ; z |-> y]
}
9:
{
 [w |-> z ; x |-> 2 ; y |-> 3 ; z |-> y]
}
10:
{
 [w |-> z ; x |-> 2 ; y |-> 4 ; z |-> y]
}
11:
{
 [w |-> z ; x |-> 2 ; y |-> 4 ; z |-> y]
}
12:
{
 [w |-> z ; x |-> 5 ; y |-> 4 ; 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]
"0:
{
 []
}
1:
{
 []
}
2:
{
 [w |-> 123]
}
3:
{
 [w |-> 123]
}
4:
{
 [w |-> 123 ; x |-> 2]
}
5:
{
 [w |-> 123 ; x |-> 2]
}
6:
{
 [w |-> 123 ; x |-> 2 ; y |-> 4]
}
7:
{
 [w |-> 123 ; x |-> 2 ; y |-> 4]
}
8:
{
 [w |-> 123 ; x |-> 2 ; y |-> 4 ; z |-> 3]
}
9:
{
 [w |-> 123 ; x |-> 2 ; y |-> 4 ; z |-> 3]
}
10:
{
 [v |-> x ; w |-> 123 ; x |-> 2 ; y |-> 4 ; z |-> 3]
}
11:
{
 [v |-> x ; w |-> 0 ; x |-> 0 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 4],
 [v |-> x ; w |-> 123 ; x |-> 2 ; y |-> 4 ; z |-> 3]
}
12:
{
 [v |-> x ; w |-> 0 ; x |-> 0 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 4],
 [v |-> x ; w |-> 123 ; x |-> 2 ; y |-> 4 ; z |-> 3]
}
13:
{
 [v |-> x ; w |-> 0 ; x |-> 0 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 4],
 [v |-> x ; w |-> 123 ; x |-> 2 ; y |-> 4 ; z |-> 3]
}
14:
{
 [v |-> x ; w |-> 0 ; x |-> -1 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 0 ; y |-> 5 ; z |-> 4],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 4 ; z |-> 3]
}
15:
{
 [v |-> x ; w |-> 0 ; x |-> -1 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 0 ; y |-> 5 ; z |-> 4],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 4 ; z |-> 3]
}
16:
{
 [v |-> x ; w |-> 0 ; x |-> -1 ; y |-> 7 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 0 ; y |-> 6 ; z |-> 4],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 3]
}
17:
{
 [v |-> x ; w |-> 123 ; x |-> 0 ; y |-> 6 ; z |-> 4],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 3]
}
18:
{
 [v |-> x ; w |-> 0 ; x |-> -1 ; y |-> 7 ; z |-> 5]
}
19:
{}
20:
{
 [v |-> x ; w |-> 0 ; x |-> 0 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 4]
}
21:
{
 [v |-> x ; w |-> 0 ; x |-> 0 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 4]
}
22:
{}
23:
{}
24:
{
 [v |-> x ; w |-> 123 ; x |-> 0 ; y |-> 6 ; z |-> 4],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 3]
}
25:
{
 [v |-> x ; w |-> 123 ; x |-> 0 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 4]
}
26:
{
 [v |-> x ; w |-> 123 ; x |-> 0 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 4]
}
27:
{
 [v |-> x ; w |-> 0 ; x |-> 0 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 4]
}
28:
{
 [v |-> x ; w |-> 0 ; x |-> 0 ; y |-> 6 ; z |-> 5],
 [v |-> x ; w |-> 123 ; x |-> 1 ; y |-> 5 ; z |-> 4]
}
29:
{
 [v |-> x ; w |-> 0 ; x |-> -1 ; y |-> 7 ; z |-> 5]
}
"