AbsHoudini: Tolerate some assertion failing. Updated regression baseline.

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

+)