diff options
| author |  stefanheule <unknown> | 2012-09-11 21:10:37 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-09-11 21:10:37 +0200 |
| commit | cb8cfc4d297dd9e88aca2b63742c0ecd1ef5e9a3 (patch) | |
| tree | 50c565d7bdb2f7c0dc970cf653d4c52399e480f2 /Chalice/tests | |
| parent | 31f0f61999a060976e66a7ea63db9a69acabc378 (diff) | |
Chalice: Update reference output for all test-cases due to recent change in the output.
Diffstat (limited to 'Chalice/tests')
77 files changed, 77 insertions, 77 deletions
diff --git a/Chalice/tests/examples/AVLTree.iterative.output.txt b/Chalice/tests/examples/AVLTree.iterative.output.txt index 152260e3..9b8797ef 100644 --- a/Chalice/tests/examples/AVLTree.iterative.output.txt +++ b/Chalice/tests/examples/AVLTree.iterative.output.txt @@ -1,4 +1,4 @@ Verification of AVLTree.iterative.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/AVLTree.nokeys.output.txt b/Chalice/tests/examples/AVLTree.nokeys.output.txt index c9dc557a..49850add 100644 --- a/Chalice/tests/examples/AVLTree.nokeys.output.txt +++ b/Chalice/tests/examples/AVLTree.nokeys.output.txt @@ -1,4 +1,4 @@ Verification of AVLTree.nokeys.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt index 2955a814..e7ae56f6 100644 --- a/Chalice/tests/examples/AssociationList.output.txt +++ b/Chalice/tests/examples/AssociationList.output.txt @@ -7,4 +7,4 @@ Verification of AssociationList.chalice using parameters="" 73.9: The loop might lock/unlock more than the lockchange clause allows. 107.7: Monitor invariant might hot hold. Insufficient fraction at 120.13 for Node.key. -Boogie program verifier finished with 6 errors and 0 smoke test warnings.
+Boogie program verifier finished with 6 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/BackgroundComputation.output.txt b/Chalice/tests/examples/BackgroundComputation.output.txt index dc1bafc1..ad3f590e 100644 --- a/Chalice/tests/examples/BackgroundComputation.output.txt +++ b/Chalice/tests/examples/BackgroundComputation.output.txt @@ -1,4 +1,4 @@ Verification of BackgroundComputation.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt index b47290ea..91c56769 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt @@ -5,4 +5,4 @@ Verification of CopyLessMessagePassing-with-ack.chalice using parameters="" 69.22: Assumption introduces a contradiction. 72.21: Assumption introduces a contradiction. -Boogie program verifier finished with 0 errors and 3 smoke test warnings.
+Boogie program verifier finished with 0 errors and 3 smoke test warnings
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt index 42a63bf1..2d6d752d 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt @@ -4,4 +4,4 @@ Verification of CopyLessMessagePassing-with-ack2.chalice using parameters="" 50.23: Assumption introduces a contradiction. 65.27: Assumption introduces a contradiction. -Boogie program verifier finished with 0 errors and 2 smoke test warnings.
+Boogie program verifier finished with 0 errors and 2 smoke test warnings
diff --git a/Chalice/tests/examples/CopyLessMessagePassing.output.txt b/Chalice/tests/examples/CopyLessMessagePassing.output.txt index 26784a86..2caf540b 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing.output.txt @@ -1,4 +1,4 @@ Verification of CopyLessMessagePassing.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/FictionallyDisjointCells.output.txt b/Chalice/tests/examples/FictionallyDisjointCells.output.txt index 9bc4fb68..0b8b0c4f 100644 --- a/Chalice/tests/examples/FictionallyDisjointCells.output.txt +++ b/Chalice/tests/examples/FictionallyDisjointCells.output.txt @@ -1,4 +1,4 @@ Verification of FictionallyDisjointCells.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/ForkJoin.output.txt b/Chalice/tests/examples/ForkJoin.output.txt index b1371da7..5ddd0f65 100644 --- a/Chalice/tests/examples/ForkJoin.output.txt +++ b/Chalice/tests/examples/ForkJoin.output.txt @@ -1,4 +1,4 @@ Verification of ForkJoin.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/HandOverHand.output.txt b/Chalice/tests/examples/HandOverHand.output.txt index 5d32ad2e..13ff996a 100644 --- a/Chalice/tests/examples/HandOverHand.output.txt +++ b/Chalice/tests/examples/HandOverHand.output.txt @@ -1,4 +1,4 @@ Verification of HandOverHand.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/OwickiGries.output.txt b/Chalice/tests/examples/OwickiGries.output.txt index 3a9a215b..8235b0f4 100644 --- a/Chalice/tests/examples/OwickiGries.output.txt +++ b/Chalice/tests/examples/OwickiGries.output.txt @@ -1,4 +1,4 @@ Verification of OwickiGries.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/PetersonsAlgorithm.output.txt b/Chalice/tests/examples/PetersonsAlgorithm.output.txt index eddb4927..1be5bf8c 100644 --- a/Chalice/tests/examples/PetersonsAlgorithm.output.txt +++ b/Chalice/tests/examples/PetersonsAlgorithm.output.txt @@ -5,4 +5,4 @@ Verification of PetersonsAlgorithm.chalice using parameters="" 34.5: The statements after the while-loop are unreachable. 59.5: The statements after the while-loop are unreachable. -Boogie program verifier finished with 0 errors and 3 smoke test warnings.
+Boogie program verifier finished with 0 errors and 3 smoke test warnings
diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt index 4d91605c..20a587da 100644 --- a/Chalice/tests/examples/ProdConsChannel.output.txt +++ b/Chalice/tests/examples/ProdConsChannel.output.txt @@ -1,4 +1,4 @@ Verification of ProdConsChannel.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/RockBand.output.txt b/Chalice/tests/examples/RockBand.output.txt index 94f92a6e..f505fdb3 100644 --- a/Chalice/tests/examples/RockBand.output.txt +++ b/Chalice/tests/examples/RockBand.output.txt @@ -1,4 +1,4 @@ Verification of RockBand.chalice using parameters="-checkLeaks -defaults -autoFold"
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/Sieve.output.txt b/Chalice/tests/examples/Sieve.output.txt index 3e5117d3..0e37cd00 100644 --- a/Chalice/tests/examples/Sieve.output.txt +++ b/Chalice/tests/examples/Sieve.output.txt @@ -1,4 +1,4 @@ Verification of Sieve.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/Solver.output.txt b/Chalice/tests/examples/Solver.output.txt index 1ec04d27..7b6882c5 100644 --- a/Chalice/tests/examples/Solver.output.txt +++ b/Chalice/tests/examples/Solver.output.txt @@ -1,4 +1,4 @@ Verification of Solver.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/TreeOfWorker.output.txt b/Chalice/tests/examples/TreeOfWorker.output.txt index 13932da9..fe0c3376 100644 --- a/Chalice/tests/examples/TreeOfWorker.output.txt +++ b/Chalice/tests/examples/TreeOfWorker.output.txt @@ -1,4 +1,4 @@ Verification of TreeOfWorker.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/UnboundedThreads.output.txt b/Chalice/tests/examples/UnboundedThreads.output.txt index ccb4e93c..f8a05ed9 100644 --- a/Chalice/tests/examples/UnboundedThreads.output.txt +++ b/Chalice/tests/examples/UnboundedThreads.output.txt @@ -2,4 +2,4 @@ Verification of UnboundedThreads.chalice using parameters="" 40.17: The loop invariant at 40.17 might not be preserved by the loop. Insufficient epsilons at 40.27 for C.f. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/cell.output.txt b/Chalice/tests/examples/cell.output.txt index b5ba1586..b1567d01 100644 --- a/Chalice/tests/examples/cell.output.txt +++ b/Chalice/tests/examples/cell.output.txt @@ -5,4 +5,4 @@ Verification of cell.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 135.3: The end of method main2 is unreachable. -Boogie program verifier finished with 1 errors and 1 smoke test warnings.
+Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/examples/dining-philosophers.output.txt b/Chalice/tests/examples/dining-philosophers.output.txt index bd1bd4a0..ffba722f 100644 --- a/Chalice/tests/examples/dining-philosophers.output.txt +++ b/Chalice/tests/examples/dining-philosophers.output.txt @@ -3,4 +3,4 @@ Verification of dining-philosophers.chalice using parameters="" 24.5: The statements after the while-loop are unreachable. -Boogie program verifier finished with 0 errors and 1 smoke test warnings.
+Boogie program verifier finished with 0 errors and 1 smoke test warnings
diff --git a/Chalice/tests/examples/iterator.output.txt b/Chalice/tests/examples/iterator.output.txt index a33f44db..36a72bac 100644 --- a/Chalice/tests/examples/iterator.output.txt +++ b/Chalice/tests/examples/iterator.output.txt @@ -1,4 +1,4 @@ Verification of iterator.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/iterator2.output.txt b/Chalice/tests/examples/iterator2.output.txt index 02a7f02d..a28c5785 100644 --- a/Chalice/tests/examples/iterator2.output.txt +++ b/Chalice/tests/examples/iterator2.output.txt @@ -1,4 +1,4 @@ Verification of iterator2.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/linkedlist.output.txt b/Chalice/tests/examples/linkedlist.output.txt index ce5b5844..88911e4f 100644 --- a/Chalice/tests/examples/linkedlist.output.txt +++ b/Chalice/tests/examples/linkedlist.output.txt @@ -2,4 +2,4 @@ Verification of linkedlist.chalice using parameters="" 49.39: Precondition at 47.14 might not hold. The expression at 47.31 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/list-reverse.output.txt b/Chalice/tests/examples/list-reverse.output.txt index d8e19122..6179841d 100644 --- a/Chalice/tests/examples/list-reverse.output.txt +++ b/Chalice/tests/examples/list-reverse.output.txt @@ -1,4 +1,4 @@ Verification of list-reverse.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/lseg.output.txt b/Chalice/tests/examples/lseg.output.txt index bc953113..ed31a673 100644 --- a/Chalice/tests/examples/lseg.output.txt +++ b/Chalice/tests/examples/lseg.output.txt @@ -1,4 +1,4 @@ Verification of lseg.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/examples/producer-consumer.output.txt b/Chalice/tests/examples/producer-consumer.output.txt index 55f4bf3c..f3c3a28a 100644 --- a/Chalice/tests/examples/producer-consumer.output.txt +++ b/Chalice/tests/examples/producer-consumer.output.txt @@ -4,4 +4,4 @@ Verification of producer-consumer.chalice using parameters="" 42.5: The statements after the while-loop are unreachable. 81.5: The statements after the while-loop are unreachable. -Boogie program verifier finished with 0 errors and 2 smoke test warnings.
+Boogie program verifier finished with 0 errors and 2 smoke test warnings
diff --git a/Chalice/tests/examples/swap.output.txt b/Chalice/tests/examples/swap.output.txt index 8cd3bb7c..c0e86b2a 100644 --- a/Chalice/tests/examples/swap.output.txt +++ b/Chalice/tests/examples/swap.output.txt @@ -1,4 +1,4 @@ Verification of swap.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/general-tests/ImplicitLocals.output.txt b/Chalice/tests/general-tests/ImplicitLocals.output.txt index db26bba6..8e59a2b0 100644 --- a/Chalice/tests/general-tests/ImplicitLocals.output.txt +++ b/Chalice/tests/general-tests/ImplicitLocals.output.txt @@ -1,4 +1,4 @@ Verification of ImplicitLocals.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/general-tests/LoopLockChange.output.txt b/Chalice/tests/general-tests/LoopLockChange.output.txt index 19e84f93..ccd9a36a 100644 --- a/Chalice/tests/general-tests/LoopLockChange.output.txt +++ b/Chalice/tests/general-tests/LoopLockChange.output.txt @@ -9,4 +9,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 10.5: The statements after the while-loop are unreachable. 75.5: Assumption introduces a contradiction. -Boogie program verifier finished with 3 errors and 3 smoke test warnings.
+Boogie program verifier finished with 3 errors and 3 smoke test warnings
diff --git a/Chalice/tests/general-tests/RockBand-automagic.output.txt b/Chalice/tests/general-tests/RockBand-automagic.output.txt index 2e62b457..652213d9 100644 --- a/Chalice/tests/general-tests/RockBand-automagic.output.txt +++ b/Chalice/tests/general-tests/RockBand-automagic.output.txt @@ -1,4 +1,4 @@ Verification of RockBand-automagic.chalice using parameters="-checkLeaks -defaults -autoFold -autoMagic"
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/general-tests/SmokeTestTest.output.txt b/Chalice/tests/general-tests/SmokeTestTest.output.txt index 3d1cd786..1ad5f926 100644 --- a/Chalice/tests/general-tests/SmokeTestTest.output.txt +++ b/Chalice/tests/general-tests/SmokeTestTest.output.txt @@ -20,4 +20,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 116.3: Predicate Cell.valid is equivalent to false. 121.1: Where clause of channel C is equivalent to false. -Boogie program verifier finished with 1 errors and 16 smoke test warnings.
+Boogie program verifier finished with 1 errors and 16 smoke test warnings
diff --git a/Chalice/tests/general-tests/cell-defaults.output.txt b/Chalice/tests/general-tests/cell-defaults.output.txt index 138a5717..fd748230 100644 --- a/Chalice/tests/general-tests/cell-defaults.output.txt +++ b/Chalice/tests/general-tests/cell-defaults.output.txt @@ -7,4 +7,4 @@ Verification of cell-defaults.chalice using parameters="-defaults -autoFold -aut The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 125.3: The end of method main2 is unreachable. -Boogie program verifier finished with 3 errors and 1 smoke test warnings.
+Boogie program verifier finished with 3 errors and 1 smoke test warnings
diff --git a/Chalice/tests/general-tests/counter.output.txt b/Chalice/tests/general-tests/counter.output.txt index 3c7f78b0..53bcd98d 100644 --- a/Chalice/tests/general-tests/counter.output.txt +++ b/Chalice/tests/general-tests/counter.output.txt @@ -14,4 +14,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 137.7: The begging of the lock-block is unreachable. 142.3: The end of method nestedBad3 is unreachable. -Boogie program verifier finished with 6 errors and 5 smoke test warnings.
+Boogie program verifier finished with 6 errors and 5 smoke test warnings
diff --git a/Chalice/tests/general-tests/nestedPredicates.output.txt b/Chalice/tests/general-tests/nestedPredicates.output.txt index b080c630..635ae780 100644 --- a/Chalice/tests/general-tests/nestedPredicates.output.txt +++ b/Chalice/tests/general-tests/nestedPredicates.output.txt @@ -9,4 +9,4 @@ Verification of nestedPredicates.chalice using parameters="" 88.7: Assertion might not hold. The expression at 88.14 might not evaluate to true. 90.9: Assertion might not hold. The expression at 90.16 might not evaluate to true. -Boogie program verifier finished with 8 errors and 0 smoke test warnings.
+Boogie program verifier finished with 8 errors and 0 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog1.output.txt b/Chalice/tests/general-tests/prog1.output.txt index 630ecdfa..c6c5fe0e 100644 --- a/Chalice/tests/general-tests/prog1.output.txt +++ b/Chalice/tests/general-tests/prog1.output.txt @@ -16,4 +16,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 73.3: The end of method main5 is unreachable. 78.3: The end of method main6 is unreachable. -Boogie program verifier finished with 7 errors and 6 smoke test warnings.
+Boogie program verifier finished with 7 errors and 6 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog2.output.txt b/Chalice/tests/general-tests/prog2.output.txt index 68cd4870..da8dcf22 100644 --- a/Chalice/tests/general-tests/prog2.output.txt +++ b/Chalice/tests/general-tests/prog2.output.txt @@ -9,4 +9,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 20.3: The end of method Caller1 is unreachable. 69.3: The end of method M2 is unreachable. -Boogie program verifier finished with 4 errors and 2 smoke test warnings.
+Boogie program verifier finished with 4 errors and 2 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog3.output.txt b/Chalice/tests/general-tests/prog3.output.txt index 18d05658..286b9248 100644 --- a/Chalice/tests/general-tests/prog3.output.txt +++ b/Chalice/tests/general-tests/prog3.output.txt @@ -8,4 +8,4 @@ Verification of prog3.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 191.5: The statements after the method call statement are unreachable. -Boogie program verifier finished with 4 errors and 1 smoke test warnings.
+Boogie program verifier finished with 4 errors and 1 smoke test warnings
diff --git a/Chalice/tests/general-tests/prog4.output.txt b/Chalice/tests/general-tests/prog4.output.txt index 9415df7c..4ab057dd 100644 --- a/Chalice/tests/general-tests/prog4.output.txt +++ b/Chalice/tests/general-tests/prog4.output.txt @@ -11,4 +11,4 @@ Verification of prog4.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 2.3: The end of method M is unreachable. -Boogie program verifier finished with 7 errors and 1 smoke test warnings.
+Boogie program verifier finished with 7 errors and 1 smoke test warnings
diff --git a/Chalice/tests/general-tests/quantifiers.output.txt b/Chalice/tests/general-tests/quantifiers.output.txt index 2f325c42..f05847b6 100644 --- a/Chalice/tests/general-tests/quantifiers.output.txt +++ b/Chalice/tests/general-tests/quantifiers.output.txt @@ -2,4 +2,4 @@ Verification of quantifiers.chalice using parameters="" 57.29: The heap of the callee might not be strictly smaller than the heap of the caller. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/permission-model/basic.output.txt b/Chalice/tests/permission-model/basic.output.txt index 02e7acb7..b2bf49bd 100644 --- a/Chalice/tests/permission-model/basic.output.txt +++ b/Chalice/tests/permission-model/basic.output.txt @@ -5,4 +5,4 @@ Verification of basic.chalice using parameters="" 97.3: The postcondition at 99.13 might not hold. Insufficient fraction at 99.13 for Cell.x. 148.3: The postcondition at 150.13 might not hold. Insufficient fraction at 150.13 for Cell.x. -Boogie program verifier finished with 4 errors and 0 smoke test warnings.
+Boogie program verifier finished with 4 errors and 0 smoke test warnings
diff --git a/Chalice/tests/permission-model/channels.output.txt b/Chalice/tests/permission-model/channels.output.txt index 159e0ee6..b2f76ab6 100644 --- a/Chalice/tests/permission-model/channels.output.txt +++ b/Chalice/tests/permission-model/channels.output.txt @@ -3,4 +3,4 @@ Verification of channels.chalice using parameters="" 8.5: The where clause at 44.24 might not hold. Insufficient fraction at 44.24 for C.f. 18.3: The postcondition at 20.13 might not hold. Insufficient fraction at 20.13 for C.f. -Boogie program verifier finished with 2 errors and 0 smoke test warnings.
+Boogie program verifier finished with 2 errors and 0 smoke test warnings
diff --git a/Chalice/tests/permission-model/locks.output.txt b/Chalice/tests/permission-model/locks.output.txt index b6ea8f80..6b3a7abe 100644 --- a/Chalice/tests/permission-model/locks.output.txt +++ b/Chalice/tests/permission-model/locks.output.txt @@ -17,4 +17,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 86.3: The end of method a3 is unreachable. 138.5: The statements after the acquire statement are unreachable. -Boogie program verifier finished with 10 errors and 4 smoke test warnings.
+Boogie program verifier finished with 10 errors and 4 smoke test warnings
diff --git a/Chalice/tests/permission-model/peculiar.output.txt b/Chalice/tests/permission-model/peculiar.output.txt index e2e6ec90..07104e77 100644 --- a/Chalice/tests/permission-model/peculiar.output.txt +++ b/Chalice/tests/permission-model/peculiar.output.txt @@ -5,4 +5,4 @@ Verification of peculiar.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 30.3: The end of method t4 is unreachable. -Boogie program verifier finished with 1 errors and 1 smoke test warnings.
+Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt index f5c02b3d..b9d20e08 100644 --- a/Chalice/tests/permission-model/permission_arithmetic.output.txt +++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt @@ -19,4 +19,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 200.3: The end of method a28 is unreachable. 215.3: The end of method a28b is unreachable. -Boogie program verifier finished with 11 errors and 5 smoke test warnings.
+Boogie program verifier finished with 11 errors and 5 smoke test warnings
diff --git a/Chalice/tests/permission-model/predicates.output.txt b/Chalice/tests/permission-model/predicates.output.txt index 5c0d0455..2f4acf7b 100644 --- a/Chalice/tests/permission-model/predicates.output.txt +++ b/Chalice/tests/permission-model/predicates.output.txt @@ -8,4 +8,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 28.3: The end of method b3 is unreachable. 49.3: The end of method b5 is unreachable. -Boogie program verifier finished with 3 errors and 2 smoke test warnings.
+Boogie program verifier finished with 3 errors and 2 smoke test warnings
diff --git a/Chalice/tests/permission-model/scaling.output.txt b/Chalice/tests/permission-model/scaling.output.txt index d57ab458..f2ebfdff 100644 --- a/Chalice/tests/permission-model/scaling.output.txt +++ b/Chalice/tests/permission-model/scaling.output.txt @@ -1,4 +1,4 @@ Verification of scaling.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/permission-model/sequences.output.txt b/Chalice/tests/permission-model/sequences.output.txt index f557b8c7..7c295c9d 100644 --- a/Chalice/tests/permission-model/sequences.output.txt +++ b/Chalice/tests/permission-model/sequences.output.txt @@ -3,4 +3,4 @@ Verification of sequences.chalice using parameters="" 36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f 60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f -Boogie program verifier finished with 2 errors and 0 smoke test warnings.
+Boogie program verifier finished with 2 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt b/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt index 7239cf05..ba48d6f4 100644 --- a/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt +++ b/Chalice/tests/predicates/FoldUnfoldExperiments.output.txt @@ -1,4 +1,4 @@ Verification of FoldUnfoldExperiments.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/aux-info.output.txt b/Chalice/tests/predicates/aux-info.output.txt index ae84772b..3d873f60 100644 --- a/Chalice/tests/predicates/aux-info.output.txt +++ b/Chalice/tests/predicates/aux-info.output.txt @@ -1,4 +1,4 @@ Verification of aux-info.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/framing-fields.output.txt b/Chalice/tests/predicates/framing-fields.output.txt index 473d63f4..f1b426c6 100644 --- a/Chalice/tests/predicates/framing-fields.output.txt +++ b/Chalice/tests/predicates/framing-fields.output.txt @@ -2,4 +2,4 @@ Verification of framing-fields.chalice using parameters="" 19.5: Assertion might not hold. The expression at 19.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/framing-functions.output.txt b/Chalice/tests/predicates/framing-functions.output.txt index 01bdd7bb..2a3426c9 100644 --- a/Chalice/tests/predicates/framing-functions.output.txt +++ b/Chalice/tests/predicates/framing-functions.output.txt @@ -2,4 +2,4 @@ Verification of framing-functions.chalice using parameters="" 23.5: Assertion might not hold. The expression at 23.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt index fc4d63fa..6d2967f5 100644 --- a/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt +++ b/Chalice/tests/predicates/list-reverse-extra-unfold-fold.output.txt @@ -1,4 +1,4 @@ Verification of list-reverse-extra-unfold-fold.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/mutual-dependence.output.txt b/Chalice/tests/predicates/mutual-dependence.output.txt index a35556a9..263084ac 100644 --- a/Chalice/tests/predicates/mutual-dependence.output.txt +++ b/Chalice/tests/predicates/mutual-dependence.output.txt @@ -2,4 +2,4 @@ Verification of mutual-dependence.chalice using parameters="" 16.5: Assertion might not hold. The expression at 16.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/setset.output.txt b/Chalice/tests/predicates/setset.output.txt index c20911f0..b2e963ee 100644 --- a/Chalice/tests/predicates/setset.output.txt +++ b/Chalice/tests/predicates/setset.output.txt @@ -5,4 +5,4 @@ Verification of setset.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 27.3: The end of method main is unreachable. -Boogie program verifier finished with 1 errors and 1 smoke test warnings.
+Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/predicates/test.output.txt b/Chalice/tests/predicates/test.output.txt index 5fac82d9..8b97e503 100644 --- a/Chalice/tests/predicates/test.output.txt +++ b/Chalice/tests/predicates/test.output.txt @@ -1,4 +1,4 @@ Verification of test.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test1.output.txt b/Chalice/tests/predicates/test1.output.txt index 73be63ec..56888ecb 100644 --- a/Chalice/tests/predicates/test1.output.txt +++ b/Chalice/tests/predicates/test1.output.txt @@ -1,4 +1,4 @@ Verification of test1.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test10.output.txt b/Chalice/tests/predicates/test10.output.txt index d38b56a0..c043cbed 100644 --- a/Chalice/tests/predicates/test10.output.txt +++ b/Chalice/tests/predicates/test10.output.txt @@ -1,4 +1,4 @@ Verification of test10.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test2.output.txt b/Chalice/tests/predicates/test2.output.txt index d0bed944..780c15ef 100644 --- a/Chalice/tests/predicates/test2.output.txt +++ b/Chalice/tests/predicates/test2.output.txt @@ -1,4 +1,4 @@ Verification of test2.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test3.output.txt b/Chalice/tests/predicates/test3.output.txt index 7e4e49d6..2753e3f5 100644 --- a/Chalice/tests/predicates/test3.output.txt +++ b/Chalice/tests/predicates/test3.output.txt @@ -1,4 +1,4 @@ Verification of test3.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test4.output.txt b/Chalice/tests/predicates/test4.output.txt index 5268bec7..08a565c8 100644 --- a/Chalice/tests/predicates/test4.output.txt +++ b/Chalice/tests/predicates/test4.output.txt @@ -2,4 +2,4 @@ Verification of test4.chalice using parameters="" 54.2: Assertion might not hold. The expression at 54.9 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/test7.output.txt b/Chalice/tests/predicates/test7.output.txt index 46ac796c..e66a1d75 100644 --- a/Chalice/tests/predicates/test7.output.txt +++ b/Chalice/tests/predicates/test7.output.txt @@ -13,4 +13,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 62.3: The end of method uf0 is unreachable. 86.3: The end of method uf3 is unreachable. -Boogie program verifier finished with 7 errors and 3 smoke test warnings.
+Boogie program verifier finished with 7 errors and 3 smoke test warnings
diff --git a/Chalice/tests/predicates/test8.output.txt b/Chalice/tests/predicates/test8.output.txt index 881b2ef0..567d2894 100644 --- a/Chalice/tests/predicates/test8.output.txt +++ b/Chalice/tests/predicates/test8.output.txt @@ -1,4 +1,4 @@ Verification of test8.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/predicates/unfolding.output.txt b/Chalice/tests/predicates/unfolding.output.txt index 4a1ebbde..7ff49106 100644 --- a/Chalice/tests/predicates/unfolding.output.txt +++ b/Chalice/tests/predicates/unfolding.output.txt @@ -2,4 +2,4 @@ Verification of unfolding.chalice using parameters="" 12.5: Assertion might not hold. The expression at 12.12 might not evaluate to true. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/internal-bug-1.output.txt b/Chalice/tests/regressions/internal-bug-1.output.txt index ea14d3e3..7685b77a 100644 --- a/Chalice/tests/regressions/internal-bug-1.output.txt +++ b/Chalice/tests/regressions/internal-bug-1.output.txt @@ -1,4 +1,4 @@ Verification of internal-bug-1.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/internal-bug-2.output.txt b/Chalice/tests/regressions/internal-bug-2.output.txt index 3b763659..8724af64 100644 --- a/Chalice/tests/regressions/internal-bug-2.output.txt +++ b/Chalice/tests/regressions/internal-bug-2.output.txt @@ -5,4 +5,4 @@ Verification of internal-bug-2.chalice using parameters="" The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 6.5: The end of method koko is unreachable. -Boogie program verifier finished with 1 errors and 1 smoke test warnings.
+Boogie program verifier finished with 1 errors and 1 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10192.output.txt b/Chalice/tests/regressions/workitem-10192.output.txt index 1f5fbeec..f2a5b539 100644 --- a/Chalice/tests/regressions/workitem-10192.output.txt +++ b/Chalice/tests/regressions/workitem-10192.output.txt @@ -1,4 +1,4 @@ Verification of workitem-10192.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10194.output.txt b/Chalice/tests/regressions/workitem-10194.output.txt index 580a8068..23114b0a 100644 --- a/Chalice/tests/regressions/workitem-10194.output.txt +++ b/Chalice/tests/regressions/workitem-10194.output.txt @@ -3,4 +3,4 @@ Verification of workitem-10194.chalice using parameters="" 20.35: Location might not be readable. 35.3: Assertion might not hold. The expression at 35.10 might not evaluate to true. -Boogie program verifier finished with 2 errors and 0 smoke test warnings.
+Boogie program verifier finished with 2 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10195.output.txt b/Chalice/tests/regressions/workitem-10195.output.txt index 0636df17..6e8b3556 100644 --- a/Chalice/tests/regressions/workitem-10195.output.txt +++ b/Chalice/tests/regressions/workitem-10195.output.txt @@ -9,4 +9,4 @@ The program did not fully verify; the smoke warnings might be misleading if cont 19.9: Precondition of method succeeds2 is equivalent to false. 27.9: Precondition of method fails2 is equivalent to false. -Boogie program verifier finished with 2 errors and 4 smoke test warnings.
+Boogie program verifier finished with 2 errors and 4 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10196.output.txt b/Chalice/tests/regressions/workitem-10196.output.txt index 013880cc..26199999 100644 --- a/Chalice/tests/regressions/workitem-10196.output.txt +++ b/Chalice/tests/regressions/workitem-10196.output.txt @@ -1,4 +1,4 @@ Verification of workitem-10196.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10197.output.txt b/Chalice/tests/regressions/workitem-10197.output.txt index 9cc1319a..c83bbfe0 100644 --- a/Chalice/tests/regressions/workitem-10197.output.txt +++ b/Chalice/tests/regressions/workitem-10197.output.txt @@ -1,4 +1,4 @@ Verification of workitem-10197.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10198.output.txt b/Chalice/tests/regressions/workitem-10198.output.txt index 8e421059..c3b59307 100644 --- a/Chalice/tests/regressions/workitem-10198.output.txt +++ b/Chalice/tests/regressions/workitem-10198.output.txt @@ -2,4 +2,4 @@ Verification of workitem-10198.chalice using parameters="" 12.2: Method might lock/unlock more than allowed. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10199.output.txt b/Chalice/tests/regressions/workitem-10199.output.txt index 4fb873e7..660fd6ae 100644 --- a/Chalice/tests/regressions/workitem-10199.output.txt +++ b/Chalice/tests/regressions/workitem-10199.output.txt @@ -1,4 +1,4 @@ Verification of workitem-10199.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10200.output.txt b/Chalice/tests/regressions/workitem-10200.output.txt index cac4bb62..90d5b467 100644 --- a/Chalice/tests/regressions/workitem-10200.output.txt +++ b/Chalice/tests/regressions/workitem-10200.output.txt @@ -2,4 +2,4 @@ Verification of workitem-10200.chalice using parameters="" 7.15: The heap of the callee might not be strictly smaller than the heap of the caller. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-10223.output.txt b/Chalice/tests/regressions/workitem-10223.output.txt index f4bfd78d..b65fbc0c 100644 --- a/Chalice/tests/regressions/workitem-10223.output.txt +++ b/Chalice/tests/regressions/workitem-10223.output.txt @@ -1,4 +1,4 @@ Verification of workitem-10223.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-8234.output.txt b/Chalice/tests/regressions/workitem-8234.output.txt index 8d13e17a..14175fd2 100644 --- a/Chalice/tests/regressions/workitem-8234.output.txt +++ b/Chalice/tests/regressions/workitem-8234.output.txt @@ -1,4 +1,4 @@ Verification of workitem-8234.chalice using parameters=""
-Boogie program verifier finished with 0 errors and 0 smoke test warnings.
+Boogie program verifier finished with 0 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-8236.output.txt b/Chalice/tests/regressions/workitem-8236.output.txt index 30b42ab1..6f1994d3 100644 --- a/Chalice/tests/regressions/workitem-8236.output.txt +++ b/Chalice/tests/regressions/workitem-8236.output.txt @@ -2,4 +2,4 @@ Verification of workitem-8236.chalice using parameters="" 3.2: Method might lock/unlock more than allowed. -Boogie program verifier finished with 1 errors and 0 smoke test warnings.
+Boogie program verifier finished with 1 errors and 0 smoke test warnings
diff --git a/Chalice/tests/regressions/workitem-9978.output.txt b/Chalice/tests/regressions/workitem-9978.output.txt index 0e557a3b..e6086625 100644 --- a/Chalice/tests/regressions/workitem-9978.output.txt +++ b/Chalice/tests/regressions/workitem-9978.output.txt @@ -3,4 +3,4 @@ Verification of workitem-9978.chalice using parameters="" 4.5: The statements after the while-loop are unreachable. -Boogie program verifier finished with 0 errors and 1 smoke test warnings.
+Boogie program verifier finished with 0 errors and 1 smoke test warnings
|