bug fix in houdini

also fixed runtest.bat and Answer

3 files changed, 6 insertions, 37 deletions

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 1b03c507..79c6fb77 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -268,7 +268,7 @@ namespace Microsoft.Boogie.Houdini {
       Dictionary<Implementation, HoudiniVCGen> vcgenSessions = new Dictionary<Implementation, HoudiniVCGen>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Implementation impl = decl as Implementation;

-        if (impl != null) {

+        if (impl != null && !impl.SkipVerification) {

           impls.Add(impl);

         }

       }

@@ -309,13 +309,13 @@ namespace Microsoft.Boogie.Houdini {
       } 

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Implementation impl = decl as Implementation;

-        if (impl == null) continue;

+        if (impl == null || impl.SkipVerification) continue;

         callGraph.AddSource(impl);

         procToImpls[impl.Proc].Add(impl);

       }

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Implementation impl = decl as Implementation;

-        if (impl == null) continue;

+        if (impl == null || impl.SkipVerification) continue;

         foreach (Block b in impl.Blocks) {

           foreach (Cmd c in b.Cmds) {

             CallCmd cc = c as CallCmd;

@@ -333,9 +333,8 @@ namespace Microsoft.Boogie.Houdini {
       Queue<Implementation> queue = new Queue<Implementation>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Implementation impl = decl as Implementation;

-        if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {

-          queue.Enqueue(impl);

-        }

+        if (impl == null || impl.SkipVerification) continue;

+        queue.Enqueue(impl);

       }

       return queue;

     }

diff --git a/Test/houdini/Answer b/Test/houdini/Answer
index 8c0f30ea..d29caa5c 100644
--- a/Test/houdini/Answer
+++ b/Test/houdini/Answer
@@ -4,14 +4,6 @@
 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

 

@@ -40,36 +32,14 @@ Boogie program verifier finished with 2 verified, 0 errors
 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

 

diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat
index ae82455a..2a391b2c 100644
--- a/Test/houdini/runtest.bat
+++ b/Test/houdini/runtest.bat
@@ -6,6 +6,6 @@ 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

+  %BGEXE% %* /nologo /contractInfer %%f

 rem  %BGEXE% %* /nologo /prover:z3api /Houdini:ci %%f

 )