blob: 3d1cd786a51b8a4bdd48f78c92ba71bbffa26fcb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Verification of SmokeTestTest.chalice using parameters=""
106.3: The postcondition at 107.13 might not hold. The expression at 107.13 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.
2.1: Monitor invariant is equivalent to false.
8.3: Precondition of method a1 is equivalent to false.
12.3: Precondition of method a2 is equivalent to false.
27.5: The begging of the if-branch is unreachable.
43.5: The begging of the if-branch is unreachable.
53.5: Assumption introduces a contradiction.
59.5: The statements after the while-loop are unreachable.
76.5: The begging of the else-branch is unreachable.
83.3: Precondition of function f1 is equivalent to false.
90.5: The begging of the if-branch is unreachable.
93.7: The begging of the else-branch is unreachable.
93.19: Assumption introduces a contradiction.
100.5: Assumption introduces a contradiction.
113.5: The statements after the method call statement are unreachable.
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.
|
