summaryrefslogtreecommitdiff
path: root/Test/houdini
diff options
context:
space:
mode:
authorGravatar mikebarnett <unknown>2009-07-15 21:03:41 +0000
committerGravatar mikebarnett <unknown>2009-07-15 21:03:41 +0000
commitce1c2de044c91624370411e23acab13b0381949b (patch)
tree592539996fe08050ead5ee210c973801611dde40 /Test/houdini
Initial set of files.
Diffstat (limited to 'Test/houdini')
-rw-r--r--Test/houdini/Answer78
-rw-r--r--Test/houdini/houd1.bpl19
-rw-r--r--Test/houdini/houd10.bpl23
-rw-r--r--Test/houdini/houd11.bpl13
-rw-r--r--Test/houdini/houd12.bpl58
-rw-r--r--Test/houdini/houd2.bpl27
-rw-r--r--Test/houdini/houd3.bpl27
-rw-r--r--Test/houdini/houd4.bpl27
-rw-r--r--Test/houdini/houd5.bpl29
-rw-r--r--Test/houdini/houd6.bpl44
-rw-r--r--Test/houdini/houd7.bpl35
-rw-r--r--Test/houdini/houd8.bpl30
-rw-r--r--Test/houdini/houd9.bpl32
-rw-r--r--Test/houdini/runtest.bat11
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
+)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 23:16:20 +0000