blob: da8dcf220886eb2d8eaad90cce1d3910a8f388ff (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Verification of prog2.chalice using parameters=""
24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.
31.13: Location might not be readable.
72.5: Const variable can be assigned to only once.
77.5: Assertion might not hold. The expression at 77.12 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.
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
|
