[Header]
open Program
open SwHell

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
  ((hellAnalyzer (pgm)))



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

test_output
"
liberation := 0;
x := read; 
y := 100; 
p := &y;
if (x < 100)
  then x := 100
  else liberation := *p + (-99)
"

[Value]
YES

[Test]
(* hell2.k : if *)
test_output
"
liberation := 0;
a := read;
if (a < 1000)
  then b := 10
  else b := 30;
if (b < 20)
  then liberation := 1
  else liberation := 0
"

[Value]
NO

[Test]
(* hell3.k : Simple loop *)

test_output
"
x := 0;
i := read;
while(x < 99)
do(
  x := x + 1
);
if (x < i)
  then liberation := 1
  else liberation := 0
"

[Value]
YES

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

test_output
"
liberation := 0;
a := 0;
b := read;
if (b < 1000) 
  then a := 10
  else a := 20;
if (a < 30)
  then liberation := 1 
  else (if (99 < 100) then liberation := 0 else liberation := 1) (* unreachable *)
"

[Value]
YES

[Test]
(* hell5.k : More complex loop pruning. *)

test_output
"
liberation := 0;
x := read;
sum := 0;
while(sum < x)
do(
  sum := sum + 1
);
if(99 < sum)
  then liberation := 1
  else liberation := 0
"

[Value]
YES


[Test]
(* hell6.k Weak update *)

test_output
"
liberation := 0;
a := read;
if (a < 1000) 
  then (p := &liberation) 
  else (p := &a);
*p := 1
"

[Value]
NO

[Test]
(* hell7.k : join + loop (difficult) *)

test_output
"
liberation := 1;
i := read;
s := 0;

while ( s < i )
do(
  b := false;
  s := s + 1;
  if (b)
    then i := i + 1
    else
      (if ( s < 100)
        then (p := &liberation)
        else  p :=  &i)
  );
  *p := 0  (* p can’t point liberation if read > 99*)
"

[Value]
YES


[Test]
(* hell8.k : join + loop (difficult 2) *)

test_output
"
liberation := 0;
a := 0;
i := read;
while (a < i)
do
  a := a + 1;
if (i < 100)
then(
  n := &liberation
)
else(
n := 0;
  while( n < i )
  do(
    liberation := liberation + 1;
    n := n+1;
    if (n < i)
        then liberation := liberation + (-1)
        else liberation := liberation   (* liberation becomes 1 *)
  );
  n := &i
);
*n := 0 (* n can’t point liberation *)
"

[Value]
YES