Fix tests

Test/test0/Prune.bpl → Test/pruning/Automatic.bpl

@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie /pruneFunctionsAndAxioms "%s" > "%t"
+// RUN: %parallel-boogie /prune:1 /errorTrace:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function {:exclude_dep} f1 (x: int) : int;
@@ -24,14 +24,6 @@ procedure I1(x : int) returns (y: int)
  // is thus removed from the outgoing set of I1.
  // This makes the axiom on line 23 unreachable from I1, which is thus pruned away.
 {
- var i: int where false;
-
- if (x > 0) {
- havoc i; // mentioning i in this branch results in assuming false because of the where clause.
- // Thus, the post-condition proves for this path.
- } else {
- assume {:focus} true; // i is not mentioned in this branch so the where clause is not assumed for it.
- }
 }
 
 procedure I2(x : int) returns (y: int)

Test/pruning/Automatic.bpl.expect

@@ -0,0 +1,6 @@
+Automatic.bpl(27,1): Error: A postcondition might not hold on this return path.
+Automatic.bpl(23,3): Related location: This is the postcondition that might not hold.
+Automatic.bpl(57,1): Error: A postcondition might not hold on this return path.
+Automatic.bpl(55,3): Related location: This is the postcondition that might not hold.
+
+Boogie program verifier finished with 1 verified, 2 errors

Test/pruning/Basic.bpl.expect

@@ -0,0 +1,6 @@
+Basic.bpl(29,1): Error: A postcondition might not hold on this return path.
+Basic.bpl(25,3): Related location: This is the postcondition that might not hold.
+Basic.bpl(29,1): Error: A postcondition might not hold on this return path.
+Basic.bpl(26,3): Related location: This is the postcondition that might not hold.
+
+Boogie program verifier finished with 1 verified, 2 errors

Test/pruning/Focus.bpl

@@ -0,0 +1,47 @@
+// RUN: %parallel-boogie /vcsDumpSplits /errorTrace:0 "%s" > "%t"
+// RUN: mv %/S/Ex.split* %/S/Output/
+// RUN: %diff "%s.expect" "%t"
+// RUN: %diff ./Output/Ex.split.0.bpl ./Output/Ex.split.0.bpl
+// RUN: %diff ./Output/Ex.split.1.bpl ./Output/Ex.split.1.bpl
+// RUN: %diff ./Output/Ex.split.2.bpl ./Output/Ex.split.2.bpl
+// RUN: %diff ./Output/Ex.split.3.bpl ./Output/Ex.split.3.bpl
+// RUN: %diff ./Output/Ex.split.4.bpl ./Output/Ex.split.4.bpl
+// RUN: %diff ./Output/Ex.split.5.bpl ./Output/Ex.split.5.bpl
+
+procedure Ex() returns (y: int)
+ ensures y >= 0;
+{
+ var x: int;
+ x := 5;
+ y := 0;
+ while (x > 0)
+ invariant x + y == 5;
+ invariant x*x <= 25;
+ {
+ x := x - 1;
+ assert {:split_here} (x+y) * (x+y) > 16; // should not lead to more than one split.
+ assert {:focus} (x+y) * (x+y) > 25;
+ y := y + 1;
+ if (x < 3) {
+ assert 2 < 2;
+ assert {:focus} y*y > 4;
+ }
+ else {
+ assert 2 < 2;
+ }
+ assert {:focus} (x+y) * (x+y) == 25;
+ }
+}
+
+procedure focusInconsistency(x : int) returns (y: int)
+ ensures false;
+{
+ var i: int where false;
+
+ if (x > 0) {
+ havoc i; // mentioning i in this branch results in assuming false because of the where clause.
+ // Thus, the post-condition proves for this path.
+ } else {
+ assume {:focus} true; // i is not mentioned in this branch so the where clause is not assumed for it.
+ }
+}

Test/pruning/Focus.bpl.expect

@@ -0,0 +1,3 @@
+Focus.bpl(22,5): Error: This assertion might not hold.
+
+Boogie program verifier finished with 1 verified, 1 error