14 files changed, 453 insertions, 0 deletions
diff --git a/Test/houdini/Answer b/Test/houdini/Answer
new file mode 100644
index 00000000..8c0f30ea
--- /dev/null
+++ b/Test/houdini/Answer
@@ -0,0 +1,78 @@
+
+-------------------- houd1.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- houd2.bpl --------------------
+----------------------------------------
+Functions: Errors
+	bar
+----------------------------------------
+houd2.bpl(12,1): Error BP5003: A postcondition might not hold at this return statement.
+houd2.bpl(9,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    houd2.bpl(11,3): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+
+-------------------- houd3.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- houd4.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- houd5.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- houd6.bpl --------------------
+
+Boogie program verifier finished with 3 verified, 0 errors
+
+-------------------- houd7.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- houd8.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- houd9.bpl --------------------
+----------------------------------------
+Functions: Errors
+	foo
+----------------------------------------
+houd9.bpl(19,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    houd9.bpl(18,9): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- houd10.bpl --------------------
+----------------------------------------
+Functions: Errors
+	foo
+----------------------------------------
+houd10.bpl(15,3): Error BP5002: A precondition for this call might not hold.
+houd10.bpl(20,1): Related location: This is the precondition that might not hold.
+Execution trace:
+    houd10.bpl(14,9): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- houd11.bpl --------------------
+----------------------------------------
+Functions: Errors
+	foo
+----------------------------------------
+houd11.bpl(8,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    houd11.bpl(7,9): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- houd12.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/houdini/houd1.bpl b/Test/houdini/houd1.bpl
new file mode 100644
index 00000000..4acea845
--- /dev/null
+++ b/Test/houdini/houd1.bpl
@@ -0,0 +1,19 @@
+const {:existential true} b1:bool;
+
+var myVar: int;
+
+procedure foo (i:int)
+modifies myVar;
+// comment
+ensures b1 ==> myVar>0;
+ensures myVar!=-1;
+{
+  if (i>0) {
+    myVar := 5;
+  } else {
+    myVar := 0;
+  }
+}
+
+// expected output: Correct
+// expected end assigment: b1->False 
+\ No newline at end of file
diff --git a/Test/houdini/houd10.bpl b/Test/houdini/houd10.bpl
new file mode 100644
index 00000000..1eea1691
--- /dev/null
+++ b/Test/houdini/houd10.bpl
@@ -0,0 +1,23 @@
+const {:existential true} b1:bool;
+const {:existential true} b2:bool;
+const {:existential true} b3:bool;
+
+var fooVar: int;
+var xVar: int;
+
+procedure foo() 
+modifies fooVar;
+modifies xVar;
+ensures b1 ==> fooVar==0;
+ensures b3 ==> xVar<0;
+{
+  fooVar:=5; 
+  call bar();
+}
+
+procedure bar(); 
+modifies xVar;
+requires fooVar!=5;
+
+// expected outcome: Errors
+// expected assigment: b1->True,b2->True,b3->True
+\ No newline at end of file
diff --git a/Test/houdini/houd11.bpl b/Test/houdini/houd11.bpl
new file mode 100644
index 00000000..df9f9e3f
--- /dev/null
+++ b/Test/houdini/houd11.bpl
@@ -0,0 +1,13 @@
+
+var fooVar: int;
+
+procedure foo() 
+modifies fooVar;
+{
+  fooVar:=5; 
+  assert(fooVar==4);
+  assert(fooVar==3);
+}
+
+// expected outcome: Errors
+// expected assigment: []
+\ No newline at end of file
diff --git a/Test/houdini/houd12.bpl b/Test/houdini/houd12.bpl
new file mode 100644
index 00000000..f3152720
--- /dev/null
+++ b/Test/houdini/houd12.bpl
@@ -0,0 +1,58 @@
+// Example to test candidate annotations on loops
+
+const {:existential true} b1:bool;
+const {:existential true} b2:bool;
+const {:existential true} b3:bool;
+const {:existential true} b4:bool;
+const {:existential true} b5:bool;
+const {:existential true} b6:bool;
+const {:existential true} b7:bool;
+
+var x: int;
+var y: int;
+
+
+procedure foo() 
+modifies x;
+modifies y;
+ensures (b4 ==> x == 0);
+ensures (b5 ==> y == 10);
+ensures (b6 ==> x == 10);
+ensures (b7 ==> y == 11);
+
+{
+  x := 10;
+  y := 0;
+
+  goto Head;
+
+Head: 
+
+  //loop invariants
+ assert (b1 ==> x < 0);
+ assert (b2 ==> x >= 0);
+ assert (b3 ==> x + y == 10);
+ goto Body, Exit;
+
+Body:
+  assume x > 0;
+  x := x - 1;
+  y := y + 1;
+
+
+  goto Head;
+
+Exit:
+  assume !(x > 0);
+  return;
+}
+
+// expected outcome: Correct
+// expected assigment: b1->False,b2->True,b3->True,b4->True, b5->True, b6->False,b7->False
+
+
+
+
+
+
+
diff --git a/Test/houdini/houd2.bpl b/Test/houdini/houd2.bpl
new file mode 100644
index 00000000..375f662e
--- /dev/null
+++ b/Test/houdini/houd2.bpl
@@ -0,0 +1,27 @@
+const {:existential true} b1:bool;
+const {:existential true} b2:bool;
+
+
+var myVar: int;
+
+procedure bar(i:int) 
+modifies myVar;
+ensures myVar>0;
+{
+  call foo(5);
+}
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1 ==> myVar>0;
+ensures myVar!=-1;
+{
+  if (i>0) {
+    myVar := 5;
+  } else {
+    myVar := 0;
+  }
+}
+
+// expected output: Errors
+// expected end assigment: b1->False b2->True
diff --git a/Test/houdini/houd3.bpl b/Test/houdini/houd3.bpl
new file mode 100644
index 00000000..4cff2cad
--- /dev/null
+++ b/Test/houdini/houd3.bpl
@@ -0,0 +1,27 @@
+const {:existential true} b1:bool;
+const {:existential true} b2:bool;
+
+
+var myVar: int;
+
+procedure bar(i:int) 
+modifies myVar;
+ensures b2==>myVar>0;
+{
+  call foo(5);
+}
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1 ==> myVar>0;
+ensures myVar!=-1;
+{
+  if (i>0) {
+    myVar := 5;
+  } else {
+    myVar := 0;
+  }
+}
+
+// expected output: Correct
+// expected end assigment: b1->False b2->False
+\ No newline at end of file
diff --git a/Test/houdini/houd4.bpl b/Test/houdini/houd4.bpl
new file mode 100644
index 00000000..9895d633
--- /dev/null
+++ b/Test/houdini/houd4.bpl
@@ -0,0 +1,27 @@
+const {:existential true} b1:bool;
+const {:existential true} b2:bool;
+const {:existential true} b3:bool;
+const {:existential true} b4:bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b2 ==> i > 0;
+ensures b3 ==> array[i] > 0;
+modifies array;
+ensures (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+    array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b4 ==> j > 0;
+modifies array;
+ensures (forall x:int :: {array[x]} (b1 && x == j) || array[x] == old(array)[x]);
+{
+    call foo(j);
+    result := array[j];	
+}
+
+// expected outcome: Correct
+// expected assignment: b1->True,b2->True,b3->True,b4->True
+\ No newline at end of file
diff --git a/Test/houdini/houd5.bpl b/Test/houdini/houd5.bpl
new file mode 100644
index 00000000..9cd9363f
--- /dev/null
+++ b/Test/houdini/houd5.bpl
@@ -0,0 +1,29 @@
+const {:existential true} b1:bool;
+const {:existential true} b2:bool;
+const {:existential true} b3:bool;
+const {:existential true} b4:bool;
+const {:existential true} b5:bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b1 ==> i == 0;
+requires b2 ==> i > 0;
+requires b3 ==> i < 0;
+ensures b4 ==> array[i] > 0;
+modifies array;
+ensures (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+    array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b5 ==> j > 0;
+modifies array;
+{
+    call foo(j);
+    result := array[j];	
+}
+
+// expected outcome: Correct
+// expected assigment: b1->False,b2->true,b3->False,b4->True,b5->True
+\ No newline at end of file
diff --git a/Test/houdini/houd6.bpl b/Test/houdini/houd6.bpl
new file mode 100644
index 00000000..09f2dd0e
--- /dev/null
+++ b/Test/houdini/houd6.bpl
@@ -0,0 +1,44 @@
+const {:existential true} b1:bool;
+const {:existential true} b2:bool;
+const {:existential true} b3:bool;
+const {:existential true} b4:bool;
+const {:existential true} b5:bool;
+const {:existential true} b6:bool;
+const {:existential true} b7:bool;
+const {:existential true} b8:bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b6 ==> i < 0;
+requires b5 ==> i == 0;
+requires b2 ==> i > 0;
+ensures b3 ==> array[i] > 0;
+modifies array;
+ensures (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+    array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b8 ==> j < 0;
+requires b7 ==> j == 0;
+requires b4 ==> j > 0;
+modifies array;
+ensures (forall x:int :: {array[x]} (x == j) || array[x] == old(array)[x]);
+ensures (b1 ==> array[j] == old(array)[j]);
+{
+    call foo(j);
+    result := array[j];	
+}
+
+var p:int;
+
+procedure main() returns (result: int) 
+modifies array;
+{
+  call result:= bar(p);
+}
+
+// expected outcome: Correct
+// expected assigment: bi->True forall i
+\ No newline at end of file
diff --git a/Test/houdini/houd7.bpl b/Test/houdini/houd7.bpl
new file mode 100644
index 00000000..aaa1971d
--- /dev/null
+++ b/Test/houdini/houd7.bpl
@@ -0,0 +1,35 @@
+const {:existential true} b1:bool;
+const {:existential true} b2:bool;
+const {:existential true} b3:bool;
+
+var myVar: int;
+
+procedure foo(i:int) 
+requires b1 ==> i>0;
+requires b2 ==> i==0;
+requires b3 ==> i<0;
+modifies myVar;
+ensures myVar>0;
+{
+  myVar:=5; 
+}
+
+procedure bar(i:int) 
+modifies myVar;
+{
+  call foo(5);
+}
+// expected outcome: Correct
+// expected Assigment: b1->True,b2->False,b3->False
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Test/houdini/houd8.bpl b/Test/houdini/houd8.bpl
new file mode 100644
index 00000000..b57ef305
--- /dev/null
+++ b/Test/houdini/houd8.bpl
@@ -0,0 +1,30 @@
+const {:existential true} b1:bool;
+const {:existential true} b2:bool;
+const {:existential true} b3:bool;
+
+var myVar: int;
+
+procedure foo(i:int) 
+modifies myVar;
+ensures b1 ==> myVar>0;
+ensures b2 ==> myVar==0;
+ensures b3 ==> myVar<0;
+{
+  myVar:=5; 
+}
+
+// expected outcome: Correct
+// expected assigment: b1->True,b2->False,b3->False
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Test/houdini/houd9.bpl b/Test/houdini/houd9.bpl
new file mode 100644
index 00000000..a43a2bbb
--- /dev/null
+++ b/Test/houdini/houd9.bpl
@@ -0,0 +1,32 @@
+const {:existential true} b1:bool;
+const {:existential true} b2:bool;
+const {:existential true} b3:bool;
+
+axiom(b1 && b2 && b3);
+
+var fooVar: int;
+var xVar: int;
+
+
+procedure foo() 
+modifies fooVar;
+modifies xVar;
+ensures b1 ==> fooVar>0;
+ensures b2 ==> fooVar==0;
+ensures b3 ==> xVar<0;
+{
+  fooVar:=5; 
+  assert(fooVar>5);
+  xVar:=0;
+  assert(xVar>0);
+}
+
+// expected outcome: Errors
+// expected assigment: b1->True,b2->True,b3->True
+
+
+
+
+
+
+
diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat
new file mode 100644
index 00000000..ae82455a
--- /dev/null
+++ b/Test/houdini/runtest.bat
@@ -0,0 +1,11 @@
+@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+
+for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd9.bpl houd10.bpl houd11.bpl houd12.bpl) do (
+  echo.
+  echo -------------------- %%f --------------------
+  %BGEXE% %* /nologo /prover:z3 /Houdini:ci %%f
+rem  %BGEXE% %* /nologo /prover:z3api /Houdini:ci %%f
+)