diff options
| author |  stefanheule <unknown> | 2011-08-03 11:24:50 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-08-03 11:24:50 +0200 |
| commit | 80c0bd8588517ff286ec3188e124b9cd5d1b0eed (patch) | |
| tree | d3cfe082bbfab7321e45ab75495bf78663af401e /Chalice/tests/examples | |
| parent | 4ebc8d355391100fe194da9bfcc7095269677dac (diff) | |
Chalice: only show warning about misleading smoke warnings if there are actually smoke warnings.
Diffstat (limited to 'Chalice/tests/examples')
| -rw-r--r-- | Chalice/tests/examples/UnboundedThreads.output.txt | 1 | ||||
| -rw-r--r-- | Chalice/tests/examples/linkedlist.output.txt | 1 | ||||
| -rw-r--r-- | Chalice/tests/examples/quantifiers.output.txt | 1 |
3 files changed, 0 insertions, 3 deletions
diff --git a/Chalice/tests/examples/UnboundedThreads.output.txt b/Chalice/tests/examples/UnboundedThreads.output.txt index bd34d380..ccb4e93c 100644 --- a/Chalice/tests/examples/UnboundedThreads.output.txt +++ b/Chalice/tests/examples/UnboundedThreads.output.txt @@ -2,5 +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. -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. Boogie program verifier finished with 1 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/examples/linkedlist.output.txt b/Chalice/tests/examples/linkedlist.output.txt index 468e5921..ce5b5844 100644 --- a/Chalice/tests/examples/linkedlist.output.txt +++ b/Chalice/tests/examples/linkedlist.output.txt @@ -2,5 +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. -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. Boogie program verifier finished with 1 errors and 0 smoke test warnings.
diff --git a/Chalice/tests/examples/quantifiers.output.txt b/Chalice/tests/examples/quantifiers.output.txt index 4abb22e1..2f325c42 100644 --- a/Chalice/tests/examples/quantifiers.output.txt +++ b/Chalice/tests/examples/quantifiers.output.txt @@ -2,5 +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. -The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. Boogie program verifier finished with 1 errors and 0 smoke test warnings.
|