Enable houdini lit tests. Note some still fail due to Boogie

outputing absolute paths to .bpl files in error messages

37 files changed, 190 insertions, 19 deletions

diff --git a/Test/houdini/Answer b/Test/houdini/Answer
index d7edbce6..a5eab2fe 100644
--- a/Test/houdini/Answer
+++ b/Test/houdini/Answer
@@ -9,10 +9,10 @@ Boogie program verifier finished with 1 verified, 0 errors
 Assignment computed by Houdini:

 b1 = False

 b2 = True

-houd2.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.

-houd2.bpl(9,1): Related location: This is the postcondition that might not hold.

+houd2.bpl(14,1): Error BP5003: A postcondition might not hold on this return path.

+houd2.bpl(11,1): Related location: This is the postcondition that might not hold.

 Execution trace:

-    houd2.bpl(11,3): anon0

+    houd2.bpl(13,3): anon0

 

 Boogie program verifier finished with 1 verified, 1 error

 

@@ -76,9 +76,9 @@ Assignment computed by Houdini:
 b1 = True

 b2 = True

 b3 = True

-houd9.bpl(19,3): Error BP5001: This assertion might not hold.

+houd9.bpl(21,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    houd9.bpl(18,9): anon0

+    houd9.bpl(20,9): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -87,18 +87,18 @@ Assignment computed by Houdini:
 b1 = True

 b2 = True

 b3 = True

-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.

+houd10.bpl(17,3): Error BP5002: A precondition for this call might not hold.

+houd10.bpl(22,1): Related location: This is the precondition that might not hold.

 Execution trace:

-    houd10.bpl(14,9): anon0

+    houd10.bpl(16,9): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- houd11.bpl --------------------

 Assignment computed by Houdini:

-houd11.bpl(8,3): Error BP5001: This assertion might not hold.

+houd11.bpl(10,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    houd11.bpl(7,9): anon0

+    houd11.bpl(9,9): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

diff --git a/Test/houdini/houd1.bpl b/Test/houdini/houd1.bpl
index 4acea845..91ff47d4 100644
--- a/Test/houdini/houd1.bpl
+++ b/Test/houdini/houd1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 const {:existential true} b1:bool;

 

 var myVar: int;

@@ -16,4 +18,4 @@ ensures myVar!=-1;
 }

 

 // expected output: Correct

-// expected end assigment: b1->False 
\ No newline at end of file
+// expected end assigment: b1->False 

diff --git a/Test/houdini/houd1.bpl.expect b/Test/houdini/houd1.bpl.expect
new file mode 100644
index 00000000..59f1e524
--- /dev/null
+++ b/Test/houdini/houd1.bpl.expect
@@ -0,0 +1,4 @@
+Assignment computed by Houdini:
+b1 = False
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/houdini/houd10.bpl b/Test/houdini/houd10.bpl
index 1eea1691..c1e0c823 100644
--- a/Test/houdini/houd10.bpl
+++ b/Test/houdini/houd10.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 const {:existential true} b1:bool;

 const {:existential true} b2:bool;

 const {:existential true} b3:bool;

@@ -20,4 +22,4 @@ modifies xVar;
 requires fooVar!=5;

 

 // expected outcome: Errors

-// expected assigment: b1->True,b2->True,b3->True
\ No newline at end of file
+// expected assigment: b1->True,b2->True,b3->True

diff --git a/Test/houdini/houd10.bpl.expect b/Test/houdini/houd10.bpl.expect
new file mode 100644
index 00000000..36b73c58
--- /dev/null
+++ b/Test/houdini/houd10.bpl.expect
@@ -0,0 +1,10 @@
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
+houd10.bpl(17,3): Error BP5002: A precondition for this call might not hold.
+houd10.bpl(22,1): Related location: This is the precondition that might not hold.
+Execution trace:
+    houd10.bpl(16,9): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/houdini/houd11.bpl b/Test/houdini/houd11.bpl
index df9f9e3f..22f7bfd1 100644
--- a/Test/houdini/houd11.bpl
+++ b/Test/houdini/houd11.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 

 var fooVar: int;

 

@@ -10,4 +12,4 @@ modifies fooVar;
 }

 

 // expected outcome: Errors

-// expected assigment: []
\ No newline at end of file
+// expected assigment: []

diff --git a/Test/houdini/houd11.bpl.expect b/Test/houdini/houd11.bpl.expect
new file mode 100644
index 00000000..b5ea0603
--- /dev/null
+++ b/Test/houdini/houd11.bpl.expect
@@ -0,0 +1,6 @@
+Assignment computed by Houdini:
+houd11.bpl(10,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    houd11.bpl(9,9): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/houdini/houd12.bpl b/Test/houdini/houd12.bpl
index f3152720..cc6301df 100644
--- a/Test/houdini/houd12.bpl
+++ b/Test/houdini/houd12.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 // Example to test candidate annotations on loops

 

 const {:existential true} b1:bool;

diff --git a/Test/houdini/houd12.bpl.expect b/Test/houdini/houd12.bpl.expect
new file mode 100644
index 00000000..e9be1683
--- /dev/null
+++ b/Test/houdini/houd12.bpl.expect
@@ -0,0 +1,10 @@
+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/houdini/houd2.bpl b/Test/houdini/houd2.bpl
index 375f662e..1f89e762 100644
--- a/Test/houdini/houd2.bpl
+++ b/Test/houdini/houd2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 const {:existential true} b1:bool;

 const {:existential true} b2:bool;

 

diff --git a/Test/houdini/houd2.bpl.expect b/Test/houdini/houd2.bpl.expect
new file mode 100644
index 00000000..1e8d4889
--- /dev/null
+++ b/Test/houdini/houd2.bpl.expect
@@ -0,0 +1,9 @@
+Assignment computed by Houdini:
+b1 = False
+b2 = True
+houd2.bpl(14,1): Error BP5003: A postcondition might not hold on this return path.
+houd2.bpl(11,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    houd2.bpl(13,3): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/houdini/houd3.bpl b/Test/houdini/houd3.bpl
index 4cff2cad..cc634450 100644
--- a/Test/houdini/houd3.bpl
+++ b/Test/houdini/houd3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 const {:existential true} b1:bool;

 const {:existential true} b2:bool;

 

@@ -24,4 +26,4 @@ ensures myVar!=-1;
 }

 

 // expected output: Correct

-// expected end assigment: b1->False b2->False
\ No newline at end of file
+// expected end assigment: b1->False b2->False

diff --git a/Test/houdini/houd3.bpl.expect b/Test/houdini/houd3.bpl.expect
new file mode 100644
index 00000000..95c060e2
--- /dev/null
+++ b/Test/houdini/houd3.bpl.expect
@@ -0,0 +1,5 @@
+Assignment computed by Houdini:
+b1 = False
+b2 = False
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/houdini/houd4.bpl b/Test/houdini/houd4.bpl
index 9895d633..e85d6047 100644
--- a/Test/houdini/houd4.bpl
+++ b/Test/houdini/houd4.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 const {:existential true} b1:bool;

 const {:existential true} b2:bool;

 const {:existential true} b3:bool;

@@ -24,4 +26,4 @@ ensures (forall x:int :: {array[x]} (b1 && x == j) || array[x] == old(array)[x])
 }

 

 // expected outcome: Correct

-// expected assignment: b1->True,b2->True,b3->True,b4->True
\ No newline at end of file
+// expected assignment: b1->True,b2->True,b3->True,b4->True

diff --git a/Test/houdini/houd4.bpl.expect b/Test/houdini/houd4.bpl.expect
new file mode 100644
index 00000000..14fe2b50
--- /dev/null
+++ b/Test/houdini/houd4.bpl.expect
@@ -0,0 +1,7 @@
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
+b4 = True
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/houdini/houd5.bpl b/Test/houdini/houd5.bpl
index 9cd9363f..8a696a40 100644
--- a/Test/houdini/houd5.bpl
+++ b/Test/houdini/houd5.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 const {:existential true} b1:bool;

 const {:existential true} b2:bool;

 const {:existential true} b3:bool;

@@ -26,4 +28,4 @@ modifies array;
 }

 

 // expected outcome: Correct

-// expected assigment: b1->False,b2->true,b3->False,b4->True,b5->True
\ No newline at end of file
+// expected assigment: b1->False,b2->true,b3->False,b4->True,b5->True

diff --git a/Test/houdini/houd5.bpl.expect b/Test/houdini/houd5.bpl.expect
new file mode 100644
index 00000000..925b14f3
--- /dev/null
+++ b/Test/houdini/houd5.bpl.expect
@@ -0,0 +1,8 @@
+Assignment computed by Houdini:
+b1 = False
+b2 = True
+b3 = False
+b4 = True
+b5 = True
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/houdini/houd6.bpl b/Test/houdini/houd6.bpl
index 820d2d73..cf67383f 100644
--- a/Test/houdini/houd6.bpl
+++ b/Test/houdini/houd6.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 const {:existential true} b1:bool;

 const {:existential true} b2:bool;

 const {:existential true} b3:bool;

@@ -41,4 +43,4 @@ modifies array;
 }

 

 // expected outcome: Correct

-// expected assigment: bi->False forall i
\ No newline at end of file
+// expected assigment: bi->False forall i

diff --git a/Test/houdini/houd6.bpl.expect b/Test/houdini/houd6.bpl.expect
new file mode 100644
index 00000000..cf2aef34
--- /dev/null
+++ b/Test/houdini/houd6.bpl.expect
@@ -0,0 +1,11 @@
+Assignment computed by Houdini:
+b1 = False
+b2 = False
+b3 = False
+b4 = False
+b5 = False
+b6 = False
+b7 = False
+b8 = False
+
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/houdini/houd7.bpl b/Test/houdini/houd7.bpl
index aaa1971d..ba3b5cda 100644
--- a/Test/houdini/houd7.bpl
+++ b/Test/houdini/houd7.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 const {:existential true} b1:bool;

 const {:existential true} b2:bool;

 const {:existential true} b3:bool;

diff --git a/Test/houdini/houd7.bpl.expect b/Test/houdini/houd7.bpl.expect
new file mode 100644
index 00000000..2a0ab5db
--- /dev/null
+++ b/Test/houdini/houd7.bpl.expect
@@ -0,0 +1,6 @@
+Assignment computed by Houdini:
+b1 = True
+b2 = False
+b3 = False
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/houdini/houd8.bpl b/Test/houdini/houd8.bpl
index b57ef305..4b4c9afb 100644
--- a/Test/houdini/houd8.bpl
+++ b/Test/houdini/houd8.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 const {:existential true} b1:bool;

 const {:existential true} b2:bool;

 const {:existential true} b3:bool;

diff --git a/Test/houdini/houd8.bpl.expect b/Test/houdini/houd8.bpl.expect
new file mode 100644
index 00000000..72927556
--- /dev/null
+++ b/Test/houdini/houd8.bpl.expect
@@ -0,0 +1,6 @@
+Assignment computed by Houdini:
+b1 = True
+b2 = False
+b3 = False
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/houdini/houd9.bpl b/Test/houdini/houd9.bpl
index a43a2bbb..4dbfb4aa 100644
--- a/Test/houdini/houd9.bpl
+++ b/Test/houdini/houd9.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment %s > %t

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

 const {:existential true} b1:bool;

 const {:existential true} b2:bool;

 const {:existential true} b3:bool;

diff --git a/Test/houdini/houd9.bpl.expect b/Test/houdini/houd9.bpl.expect
new file mode 100644
index 00000000..05de7150
--- /dev/null
+++ b/Test/houdini/houd9.bpl.expect
@@ -0,0 +1,9 @@
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
+houd9.bpl(21,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    houd9.bpl(20,9): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/houdini/test1.bpl b/Test/houdini/test1.bpl
index e6ce06c9..89d5d50d 100644
--- a/Test/houdini/test1.bpl
+++ b/Test/houdini/test1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t

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

 var g: bool;

 

 procedure foo() 

diff --git a/Test/houdini/test1.bpl.expect b/Test/houdini/test1.bpl.expect
new file mode 100644
index 00000000..3ce36f9c
--- /dev/null
+++ b/Test/houdini/test1.bpl.expect
@@ -0,0 +1,6 @@
+Assignment computed by Houdini:
+b0 = True
+b1 = False
+b2 = False
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/houdini/test10.bpl b/Test/houdini/test10.bpl
index abb993f7..33cc54d9 100644
--- a/Test/houdini/test10.bpl
+++ b/Test/houdini/test10.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t

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

 var sdv_7: int;

 var sdv_21: int;

 const {:existential true} b1: bool;

diff --git a/Test/houdini/test10.bpl.expect b/Test/houdini/test10.bpl.expect
new file mode 100644
index 00000000..f6adc2b7
--- /dev/null
+++ b/Test/houdini/test10.bpl.expect
@@ -0,0 +1,7 @@
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
+b4 = True
+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/houdini/test2.bpl b/Test/houdini/test2.bpl
index febb28e6..99897758 100644
--- a/Test/houdini/test2.bpl
+++ b/Test/houdini/test2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t

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

 var g: int;

 var h: int;

 

diff --git a/Test/houdini/test2.bpl.expect b/Test/houdini/test2.bpl.expect
new file mode 100644
index 00000000..3ce36f9c
--- /dev/null
+++ b/Test/houdini/test2.bpl.expect
@@ -0,0 +1,6 @@
+Assignment computed by Houdini:
+b0 = True
+b1 = False
+b2 = False
+
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/houdini/test7.bpl b/Test/houdini/test7.bpl
index b5c6a4c6..be369db9 100644
--- a/Test/houdini/test7.bpl
+++ b/Test/houdini/test7.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t

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

 var g: int;

 

 procedure main() 

@@ -12,4 +14,4 @@ procedure foo()
 modifies g;

 {

   g := g + 1;

-}
\ No newline at end of file
+}

diff --git a/Test/houdini/test7.bpl.expect b/Test/houdini/test7.bpl.expect
new file mode 100644
index 00000000..81c325b2
--- /dev/null
+++ b/Test/houdini/test7.bpl.expect
@@ -0,0 +1,3 @@
+Assignment computed by Houdini:
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/houdini/test8.bpl b/Test/houdini/test8.bpl
index 12eab481..c92d63fe 100644
--- a/Test/houdini/test8.bpl
+++ b/Test/houdini/test8.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t

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

 var g: int;

 

 procedure main() 

@@ -18,4 +20,4 @@ procedure bar()
 modifies g;

 {

   g := g + 1;

-}
\ No newline at end of file
+}

diff --git a/Test/houdini/test8.bpl.expect b/Test/houdini/test8.bpl.expect
new file mode 100644
index 00000000..81c325b2
--- /dev/null
+++ b/Test/houdini/test8.bpl.expect
@@ -0,0 +1,3 @@
+Assignment computed by Houdini:
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/houdini/test9.bpl b/Test/houdini/test9.bpl
index 24eb66e8..f2eae609 100644
--- a/Test/houdini/test9.bpl
+++ b/Test/houdini/test9.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 %s > %t

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

 var v1: int;

 var v2: int;

 var v3: int;

diff --git a/Test/houdini/test9.bpl.expect b/Test/houdini/test9.bpl.expect
new file mode 100644
index 00000000..10f094b0
--- /dev/null
+++ b/Test/houdini/test9.bpl.expect
@@ -0,0 +1,19 @@
+Assignment computed by Houdini:
+b1 = False
+b2 = False
+b3 = False
+b4 = True
+b5 = False
+b6 = True
+b7 = False
+b8 = False
+b9 = False
+b10 = True
+b11 = False
+b12 = True
+b13 = False
+b14 = False
+b15 = False
+b16 = False
+
+Boogie program verifier finished with 5 verified, 0 errors