Convert houd12.bpl into a OutputCheck style test and also pass

--dump-file-to-check flag to OutputCheck by default to ease debugging

3 files changed, 13 insertions, 24 deletions

diff --git a/Test/houdini/houd12.bpl b/Test/houdini/houd12.bpl
index cc6301df..a3379a2e 100644
--- a/Test/houdini/houd12.bpl
+++ b/Test/houdini/houd12.bpl
@@ -1,20 +1,27 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

-// RUN: %diff %s.expect %t

+// RUN: %boogie -noinfer -contractInfer -printAssignment %s | %OutputCheck -d %s

 // Example to test candidate annotations on loops

 

+// CHECK-L: Assignment computed by Houdini:

+// CHECK-NEXT-L: b1 = False

 const {:existential true} b1:bool;

+// CHECK-NEXT-L: b2 = True

 const {:existential true} b2:bool;

+// CHECK-NEXT-L: b3 = True

 const {:existential true} b3:bool;

+// CHECK-NEXT-L: b4 = True

 const {:existential true} b4:bool;

+// CHECK-NEXT-L: b5 = True

 const {:existential true} b5:bool;

+// CHECK-NEXT-L: b6 = False

 const {:existential true} b6:bool;

+// CHECK-NEXT-L: b7 = False

 const {:existential true} b7:bool;

 

 var x: int;

 var y: int;

 

 

-procedure foo() 

+procedure foo()

 modifies x;

 modifies y;

 ensures (b4 ==> x == 0);

@@ -28,7 +35,7 @@ ensures (b7 ==> y == 11);
 

   goto Head;

 

-Head: 

+Head:

 

   //loop invariants

  assert (b1 ==> x < 0);

@@ -49,12 +56,4 @@ Exit:
   return;

 }

 

-// expected outcome: Correct

-// expected assigment: b1->False,b2->True,b3->True,b4->True, b5->True, b6->False,b7->False

-

-

-

-

-

-

-

+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/houdini/houd12.bpl.expect b/Test/houdini/houd12.bpl.expect
deleted file mode 100644
index e9be1683..00000000
--- a/Test/houdini/houd12.bpl.expect
+++ /dev/null
@@ -1,10 +0,0 @@
-Assignment computed by Houdini:
-b1 = False
-b2 = True
-b3 = True
-b4 = True
-b5 = True
-b6 = False
-b7 = False
-
-Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg
index 5cd4719c..cb0bb3e3 100644
--- a/Test/lit.site.cfg
+++ b/Test/lit.site.cfg
@@ -122,4 +122,4 @@ outputCheckPath = lit.util.which('OutputCheck')
 if outputCheckPath == None:
     lit_config.fatal('The OutputCheck tool is not in your PATH. Please install it.')
 
-config.substitutions.append( ('%OutputCheck', outputCheckPath) )
+config.substitutions.append( ('%OutputCheck', outputCheckPath + ' --dump-file-to-check') )