blob: 68cd48703fd1a5de521496b02d5753c497b3aa44 (
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.
|