[Header]
open Program
open Davinci

let result_leq x y =  
  match x, y with
  | _, DONTKNOW -> true
  | YES, YES -> true
  | NO, NO -> true
  | _ -> false


let test_output pgm_str = 
  (* Stdout Redirection *)
  let pgm = Parser.program Lexer.start (Lexing.from_string pgm_str) in
  ((davinciAnalyzer (pgm))) 


[Test]
(* dav1.k : Basic test with if + pointer *)

test_output
"
x := 2281;  (* 1867 + 414 *)
y := -1866; (* -1867 + 1 *)
p := &x;
q := &y;
c := read;
if (0 < c)
  then (z := *p + y)
  else (z := x + *q);
z := z + 1867
"

[Value]
YES

[Test]
(* dav2.k : if *)
test_output
"
a := 414;
b := 1;
c := 0;
d := a+b;
c := read;
if (0 < c) 
  then (d:= d + 1867) 
  else (d:= -d)
"

[Value]
NO

[Test]

(* dav3.k : Simple loop *)

test_output
"
x := 0;
while(x < 415)
do(
  x := x + 1
);
y := x;
y := y + 1867
"

[Value]
YES



[Test]
(* dav4.k : unreachable code *)

test_output
"
a:=414;
b:=1;
d:=a+b;
c := read;
if (c < 1867) 
  then (d := 10) 
  else (d := 20);
if (d < 0) 
  then (e := e + 1867) 
  else (e := e + 1000) (* This false branch cannot be taken *)
"

[Value]
YES

[Test]
(* dav5.k : Non-terminating program must be successfully analyzed, too. *)
test_output
"
x := 415;
sum := 0;
while(x < 416)
do(
  sum := sum + x;
  x := x + 1867
)
"

[Value]
YES

[Test]
(* dav6.k Weak update *)
test_output
"
c := 0;
x := 0;
y := 0;
z := 3;
c := read;
(if (0 < c) 
  then (p := &x) 
  else (p := &y));
*p := 1;
(if (x < 1) 
  then (w := z + 412)
  else (w := 100) )
"

[Value]
NO

[Test]
(* dav7.k : join + loop + dead code elim (difficult) *)
test_output
"
i := 0;
n := 415;
b := 0;

while ( i < n )
do(
  i := i+1;
  b := false;
  if (b)
    then n := 0
	else 
      (if (i < 414)
        then b := &n
        else b := &f)
);
*b := 0 (* b can't point n *) 
"

[Value]
YES

[Test]
(* dav8.k : loop + join (difficult 2) *)
test_output
"
a := 400;
i := read;
if (i < 100)
then(
  d := a + 15;
  n := 0;
  while( n < i )
  do(
    d := d + 1867; (* davinci *)
    n := n+1
  )
)
else(
  d := a + 14;
  n := 200;
  while( i < n )
  do(
    d := d + 1867; (* not davinci *)
    n := n + (-1)
  )
)
"

[Value]
NO