summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2013-05-10 14:14:21 +0530
committerGravatar akashlal <unknown>2013-05-10 14:14:21 +0530
commit89b20adf23750478098578895fef9ca3b9170927 (patch)
treeacae9d3c96ecf2ce8e236b03bce8550e5bc7e9fd /Test
parent429608680e4b6b65c9a75e9f1ca72963778983ed (diff)
AbsHoudini: Tolerate some assertion failing. Updated regression baseline.
Diffstat (limited to 'Test')
-rw-r--r--Test/AbsHoudini/Answer102
-rw-r--r--Test/AbsHoudini/fail1.bpl16
-rw-r--r--Test/AbsHoudini/runtest.bat8
3 files changed, 105 insertions, 21 deletions
diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer
index 2ba2eed3..58da416e 100644
--- a/Test/AbsHoudini/Answer
+++ b/Test/AbsHoudini/Answer
@@ -5,7 +5,7 @@ function {:existential true} {:inline} b1(x: bool) : bool
true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd2.bpl --------------------
function {:existential true} {:inline} Assert(x: bool) : bool
@@ -21,7 +21,7 @@ function {:existential true} {:inline} b2(x: bool) : bool
false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd3.bpl --------------------
function {:existential true} {:inline} Assert(x: bool) : bool
@@ -37,7 +37,7 @@ function {:existential true} {:inline} b2(x: bool) : bool
true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd4.bpl --------------------
function {:existential true} {:inline} Assert() : bool
@@ -61,7 +61,7 @@ function {:existential true} {:inline} b4(x: bool) : bool
false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd5.bpl --------------------
function {:existential true} {:inline} b1(x: bool) : bool
@@ -89,7 +89,7 @@ function {:existential true} {:inline} Assert() : bool
false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd6.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -129,7 +129,7 @@ function {:existential true} {:inline} Assert() : bool
false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd7.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -149,7 +149,7 @@ function {:existential true} {:inline} Assert() : bool
false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd8.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -165,10 +165,7 @@ function {:existential true} {:inline} b3() : bool
true
}
-Boogie program verifier finished with 0 verified, 0 errors
-
--------------------- houd9.bpl --------------------
-Error opening file "houd9.bpl": Could not find file 'C:\Users\akashl\Documents\work\boogie\Test\AbsHoudini\houd9.bpl'.
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd10.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -188,7 +185,7 @@ function {:existential true} {:inline} Assert() : bool
true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd11.bpl --------------------
function {:existential true} {:inline} Assert() : bool
@@ -196,7 +193,7 @@ function {:existential true} {:inline} Assert() : bool
true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- houd12.bpl --------------------
function {:existential true} {:inline} Assert() : bool
@@ -232,7 +229,20 @@ function {:existential true} {:inline} b7() : bool
true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- fail1.bpl --------------------
+function {:existential true} {:inline} b1(x: bool) : bool
+{
+ false
+}
+fail1.bpl(14,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ fail1.bpl(9,3): anon0
+ fail1.bpl(10,11): anon4_Then
+ fail1.bpl(14,3): anon3
+
+Boogie program verifier finished with 0 verified, 1 error
.
-------------------- test1.bpl --------------------
function {:existential true} {:inline} b0() : bool
@@ -252,7 +262,7 @@ function {:existential true} {:inline} Assert() : bool
false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test2.bpl --------------------
function {:existential true} {:inline} b0() : bool
@@ -272,7 +282,7 @@ function {:existential true} {:inline} Assert() : bool
false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test7.bpl --------------------
function {:existential true} {:inline} Assert() : bool
@@ -280,7 +290,7 @@ function {:existential true} {:inline} Assert() : bool
false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test8.bpl --------------------
function {:existential true} {:inline} Assert() : bool
@@ -288,7 +298,7 @@ function {:existential true} {:inline} Assert() : bool
false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test9.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -356,7 +366,7 @@ function {:existential true} {:inline} b16() : bool
true
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
.
-------------------- test10.bpl --------------------
function {:existential true} {:inline} b1() : bool
@@ -376,4 +386,56 @@ function {:existential true} {:inline} b4() : bool
false
}
-Boogie program verifier finished with 0 verified, 0 errors
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred1.bpl --------------------
+function {:existential true} {:inline} b0(x: bool, y: bool) : bool
+{
+ x && !y
+}
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+ (y || x) && (!x || !y)
+}
+function {:existential true} {:inline} b2(x: bool, y: bool) : bool
+{
+ x && !y
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred2.bpl --------------------
+function {:existential true} {:inline} b0(x: bool) : bool
+{
+ x
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred3.bpl --------------------
+function {:existential true} {:inline} b0(x: bool, y: bool) : bool
+{
+ x && !y
+}
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+ (y || x) && (!x || !y)
+}
+function {:existential true} {:inline} b2(x: bool, y: bool) : bool
+{
+ x && !y
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
+.
+-------------------- pred4.bpl --------------------
+function {:existential true} {:inline} b1(x: bool, y: bool) : bool
+{
+ (y || x) && (!x || !y)
+}
+function {:existential true} {:absdomain "Intervals"} {:inline} b3(x: int) : bool
+{
+ x >= 0 && x <= 0
+}
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/AbsHoudini/fail1.bpl b/Test/AbsHoudini/fail1.bpl
new file mode 100644
index 00000000..abbd015b
--- /dev/null
+++ b/Test/AbsHoudini/fail1.bpl
@@ -0,0 +1,16 @@
+function {:existential true} b1(x: bool) : bool;
+
+var myVar: int;
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1(myVar>0);
+{
+ if (i>0) {
+ myVar := 5;
+ } else {
+ myVar := 0;
+ }
+ assert false;
+}
+
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat
index 88ac1fd5..0bc74dfc 100644
--- a/Test/AbsHoudini/runtest.bat
+++ b/Test/AbsHoudini/runtest.bat
@@ -3,7 +3,7 @@ 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 (
+for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd10.bpl houd11.bpl houd12.bpl fail1.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:IA[ConstantProp] %%f
@@ -14,3 +14,9 @@ for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:IA[ConstantProp] %%f
)
+
+for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl) do (
+ echo .
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 /abstractHoudini:PredicateAbs %%f
+)