summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2013-04-18 17:50:18 +0530
committerGravatar akashlal <unknown>2013-04-18 17:50:18 +0530
commita2fcc9e7617800e2139a9cbbfa720222e4c1b6f5 (patch)
tree48d4d5b6d86968a058ffbbe9661518ec763b9204 /Test
parent308a4d37f063384cb8de166b248d9377c904e77c (diff)
Nice clean re-implementation of AbstractHoudini. And tests
Diffstat (limited to 'Test')
-rw-r--r--Test/AbsHoudini/houd1.bpl18
-rw-r--r--Test/AbsHoudini/houd10.bpl22
-rw-r--r--Test/AbsHoudini/houd11.bpl13
-rw-r--r--Test/AbsHoudini/houd12.bpl58
-rw-r--r--Test/AbsHoudini/houd2.bpl27
-rw-r--r--Test/AbsHoudini/houd3.bpl27
-rw-r--r--Test/AbsHoudini/houd4.bpl27
-rw-r--r--Test/AbsHoudini/houd5.bpl29
-rw-r--r--Test/AbsHoudini/houd6.bpl44
-rw-r--r--Test/AbsHoudini/houd7.bpl35
-rw-r--r--Test/AbsHoudini/houd8.bpl29
-rw-r--r--Test/AbsHoudini/runtest.bat9
-rw-r--r--Test/AbsHoudini/test1.bpl36
-rw-r--r--Test/AbsHoudini/test10.bpl47
-rw-r--r--Test/AbsHoudini/test2.bpl38
-rw-r--r--Test/AbsHoudini/test7.bpl15
-rw-r--r--Test/AbsHoudini/test8.bpl21
-rw-r--r--Test/AbsHoudini/test9.bpl73
18 files changed, 566 insertions, 2 deletions
diff --git a/Test/AbsHoudini/houd1.bpl b/Test/AbsHoudini/houd1.bpl
new file mode 100644
index 00000000..099c6f09
--- /dev/null
+++ b/Test/AbsHoudini/houd1.bpl
@@ -0,0 +1,18 @@
+function {:existential true} b1(x: bool) : bool;
+
+var myVar: int;
+
+procedure foo (i:int)
+modifies myVar;
+// comment
+ensures b1(myVar>0);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+}
+
+// expected output: Correct
+// expected end assigment: b1(x) = x
diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl
new file mode 100644
index 00000000..bb0c65e7
--- /dev/null
+++ b/Test/AbsHoudini/houd10.bpl
@@ -0,0 +1,22 @@
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} Assert(): 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 Assert() || fooVar!=5;
+
+// expected assigment: Assert->true,b1->True,b2->false,b3->True
diff --git a/Test/AbsHoudini/houd11.bpl b/Test/AbsHoudini/houd11.bpl
new file mode 100644
index 00000000..78087744
--- /dev/null
+++ b/Test/AbsHoudini/houd11.bpl
@@ -0,0 +1,13 @@
+function {:existential true} Assert() : bool;
+
+var fooVar: int;
+
+procedure foo()
+modifies fooVar;
+{
+ fooVar:=5;
+ assert Assert() || (fooVar==4);
+ assert Assert() || (fooVar==3);
+}
+
+// expected assigment: Assert -> true
diff --git a/Test/AbsHoudini/houd12.bpl b/Test/AbsHoudini/houd12.bpl
new file mode 100644
index 00000000..b3a1a6db
--- /dev/null
+++ b/Test/AbsHoudini/houd12.bpl
@@ -0,0 +1,58 @@
+// Example to test candidate annotations on loops
+
+function {:existential true} Assert(): bool;
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} b4():bool;
+function {:existential true} b5():bool;
+function {:existential true} b6():bool;
+function {: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 assigment: Assert -> false, b1->true,b2->false,b3->false,b4->false, b5->false, b6->true,b7->true
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/houd2.bpl b/Test/AbsHoudini/houd2.bpl
new file mode 100644
index 00000000..fd2611e2
--- /dev/null
+++ b/Test/AbsHoudini/houd2.bpl
@@ -0,0 +1,27 @@
+function {:existential true} Assert(x:bool) : bool;
+function {:existential true} b1 (x:bool):bool;
+function {:existential true} b2 (x:bool):bool;
+
+
+var myVar: int;
+
+procedure bar(i:int)
+modifies myVar;
+ensures Assert(myVar>0);
+{
+ call foo(5);
+}
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1(myVar>0);
+ensures Assert(myVar!=-1);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+}
+
+// expected end assigment: Assert(x) = true, b1(x) = true, b2(x) = false
diff --git a/Test/AbsHoudini/houd3.bpl b/Test/AbsHoudini/houd3.bpl
new file mode 100644
index 00000000..81f11018
--- /dev/null
+++ b/Test/AbsHoudini/houd3.bpl
@@ -0,0 +1,27 @@
+function {:existential true} Assert(x: bool) : bool;
+function {:existential true} b1(x: bool) : bool;
+function {:existential true} b2(x: bool) : 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 Assert(myVar!=-1);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+}
+
+// expected end assigment: Assert(x) = x, b1(x) = True, b2(x) = True
diff --git a/Test/AbsHoudini/houd4.bpl b/Test/AbsHoudini/houd4.bpl
new file mode 100644
index 00000000..01ee6707
--- /dev/null
+++ b/Test/AbsHoudini/houd4.bpl
@@ -0,0 +1,27 @@
+function {:existential true} Assert() : bool;
+function {:existential true} b1():bool;
+function {:existential true} b2(x:bool):bool;
+function {:existential true} b3(x:bool):bool;
+function {:existential true} b4(x:bool):bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b2(i > 0);
+ensures b3(array[i] > 0);
+modifies array;
+ensures Assert() || (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 Assert() || (forall x:int :: {array[x]} (!b1() && x == j) || array[x] == old(array)[x]);
+{
+ call foo(j);
+ result := array[j];
+}
+
+// expected assignment: Assert = false, b1(x) = false, b2(x) = false, b3(x) = false, b4(x) = false
diff --git a/Test/AbsHoudini/houd5.bpl b/Test/AbsHoudini/houd5.bpl
new file mode 100644
index 00000000..afbaa81c
--- /dev/null
+++ b/Test/AbsHoudini/houd5.bpl
@@ -0,0 +1,29 @@
+function {:existential true} b1(x:bool):bool;
+function {:existential true} b2(x:bool):bool;
+function {:existential true} b3(x:bool):bool;
+function {:existential true} b4(x:bool):bool;
+function {:existential true} b5():bool;
+function {:existential true} Assert():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 Assert() || (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 assigment: assert = false, b1(x) = !x, b2(x) = x, b3(x) = !x, b4(x) = x, b5() = false
diff --git a/Test/AbsHoudini/houd6.bpl b/Test/AbsHoudini/houd6.bpl
new file mode 100644
index 00000000..e4927901
--- /dev/null
+++ b/Test/AbsHoudini/houd6.bpl
@@ -0,0 +1,44 @@
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} b4():bool;
+function {:existential true} b5():bool;
+function {:existential true} b6():bool;
+function {:existential true} b7():bool;
+function {:existential true} b8():bool;
+function {:existential true} Assert(): 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 Assert() || (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 Assert() || (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 assigment: Assert -> false, bi->true forall i
diff --git a/Test/AbsHoudini/houd7.bpl b/Test/AbsHoudini/houd7.bpl
new file mode 100644
index 00000000..ef3293db
--- /dev/null
+++ b/Test/AbsHoudini/houd7.bpl
@@ -0,0 +1,35 @@
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} Assert(): bool;
+var myVar: int;
+
+procedure foo(i:int)
+requires b1() || i>0;
+requires b2() || i==0;
+requires b3() || i<0;
+modifies myVar;
+ensures Assert() || myVar>0;
+{
+ myVar:=5;
+}
+
+procedure bar(i:int)
+modifies myVar;
+{
+ call foo(5);
+}
+// expected outcome: Correct
+// expected Assigment: Assert = false, b1->false,b2->true,b3->true
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/houd8.bpl b/Test/AbsHoudini/houd8.bpl
new file mode 100644
index 00000000..8be7f3db
--- /dev/null
+++ b/Test/AbsHoudini/houd8.bpl
@@ -0,0 +1,29 @@
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {: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 assigment: b1->false,b2->true,b3->true
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat
index 34308e4e..b9816bb9 100644
--- a/Test/AbsHoudini/runtest.bat
+++ b/Test/AbsHoudini/runtest.bat
@@ -3,9 +3,14 @@ setlocal
set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (f1.bpl) do (
+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 /noinfer /contractInfer /abstractHoudini:PredicateAbs %%f
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment %%f
)
+for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
+ echo .
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 %%f
+)
diff --git a/Test/AbsHoudini/test1.bpl b/Test/AbsHoudini/test1.bpl
new file mode 100644
index 00000000..e6ce06c9
--- /dev/null
+++ b/Test/AbsHoudini/test1.bpl
@@ -0,0 +1,36 @@
+var g: bool;
+
+procedure foo()
+modifies g;
+ensures b0 ==> (!old(g) ==> old(g) == g);
+{
+ call AcquireLock();
+ call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g;
+ensures b1 ==> old(g) == g;
+{
+ g := true;
+}
+
+procedure ReleaseLock()
+modifies g;
+ensures b2 ==> old(g) == g;
+{
+ g := false;
+}
+
+procedure main()
+modifies g;
+{
+ g := false;
+ call foo();
+ assert !g;
+}
+
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true } b2: bool;
+
diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl
new file mode 100644
index 00000000..abb993f7
--- /dev/null
+++ b/Test/AbsHoudini/test10.bpl
@@ -0,0 +1,47 @@
+var sdv_7: int;
+var sdv_21: int;
+const {:existential true} b1: bool;
+const{:existential true} b2: bool;
+const{:existential true} b3: bool;
+const{:existential true} b4: bool;
+
+procedure push(a:int)
+modifies sdv_7, sdv_21;
+{
+ sdv_21 := sdv_7;
+ sdv_7 := a;
+}
+
+procedure pop()
+modifies sdv_7, sdv_21;
+{
+ sdv_7 := sdv_21;
+ havoc sdv_21;
+}
+
+procedure foo()
+modifies sdv_7, sdv_21;
+requires {:candidate} b1 ==> (sdv_7 == 0);
+ensures{:candidate} b2 ==> (sdv_7 == old(sdv_7));
+{
+ call push(2);
+ call pop();
+ call bar();
+}
+
+procedure bar()
+requires{:candidate} b3 ==> (sdv_7 == 0);
+ensures{:candidate} b4 ==> (sdv_7 == old(sdv_7));
+modifies sdv_7, sdv_21;
+{
+ call push(1);
+ call pop();
+}
+
+procedure main()
+modifies sdv_7, sdv_21;
+{
+ sdv_7 := 0;
+ call foo();
+}
+
diff --git a/Test/AbsHoudini/test2.bpl b/Test/AbsHoudini/test2.bpl
new file mode 100644
index 00000000..febb28e6
--- /dev/null
+++ b/Test/AbsHoudini/test2.bpl
@@ -0,0 +1,38 @@
+var g: int;
+var h: int;
+
+procedure foo()
+modifies g, h;
+ensures b0 ==> old(g) == g;
+{
+ call AcquireLock();
+ call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g, h;
+ensures b1 ==> old(g) == g;
+{
+ h := g;
+ g := 1;
+}
+
+procedure ReleaseLock()
+modifies g, h;
+ensures b2 ==> old(g) == g;
+{
+ g := h;
+}
+
+procedure main()
+modifies g, h;
+{
+ g := 0;
+ call foo();
+ assert g == 0;
+}
+
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true } b2: bool;
+
diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl
new file mode 100644
index 00000000..b5c6a4c6
--- /dev/null
+++ b/Test/AbsHoudini/test7.bpl
@@ -0,0 +1,15 @@
+var g: int;
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ call foo();
+ assert g == 1;
+}
+
+procedure foo()
+modifies g;
+{
+ g := g + 1;
+} \ No newline at end of file
diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl
new file mode 100644
index 00000000..12eab481
--- /dev/null
+++ b/Test/AbsHoudini/test8.bpl
@@ -0,0 +1,21 @@
+var g: int;
+
+procedure main()
+modifies g;
+{
+ g := 0;
+ call foo();
+ assert g == 1;
+}
+
+procedure {:inline 1} foo()
+modifies g;
+{
+ call bar();
+}
+
+procedure bar()
+modifies g;
+{
+ g := g + 1;
+} \ No newline at end of file
diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl
new file mode 100644
index 00000000..24eb66e8
--- /dev/null
+++ b/Test/AbsHoudini/test9.bpl
@@ -0,0 +1,73 @@
+var v1: int;
+var v2: int;
+var v3: int;
+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;
+const{:existential true} b9: bool;
+const{:existential true} b10: bool;
+const{:existential true} b11: bool;
+const{:existential true} b12: bool;
+const{:existential true} b13: bool;
+const{:existential true} b14: bool;
+const{:existential true} b15: bool;
+const{:existential true} b16: bool;
+
+procedure push()
+requires {:candidate} b1 ==> v1 == 0;
+requires {:candidate} b2 ==> v1 == 1;
+ensures {:candidate} b3 ==> v1 == 0;
+ensures {:candidate} b4 ==> v1 == 1;
+modifies v1,v2;
+{
+ v2 := v1;
+ v1 := 1;
+}
+
+procedure pop()
+modifies v1,v2;
+requires {:candidate} b5 ==> v1 == 0;
+requires {:candidate} b6 ==> v1 == 1;
+ensures {:candidate} b7 ==> v1 == 0;
+ensures {:candidate} b8 ==> v1 == 1;
+{
+ v1 := v2;
+ havoc v2;
+}
+
+procedure foo()
+modifies v1,v2;
+requires {:candidate} b9 ==> v1 == 0;
+requires {:candidate} b10 ==> v1 == 1;
+ensures {:candidate} b11 ==> v1 == 0;
+ensures {:candidate} b12 ==> v1 == 1;
+{
+ call push();
+ call pop();
+}
+
+procedure bar()
+modifies v1,v2;
+requires {:candidate} b13 ==> v1 == 0;
+requires {:candidate} b14 ==> v1 == 1;
+ensures {:candidate} b15 ==> v1 == 0;
+ensures {:candidate} b16 ==> v1 == 1;
+{
+ call push();
+ call pop();
+}
+
+procedure main()
+modifies v1,v2;
+{
+ v1 := 1;
+ call foo();
+ havoc v1;
+ call bar();
+}
+