blob: 90949273b7b6e05b71e305f2b9be5b94d39cf24e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
CallVerifiedUnder0.bpl(9,5): Error BP5002: A precondition for this call might not hold.
CallVerifiedUnder0.bpl(5,3): Related location: This is the precondition that might not hold.
Execution trace:
CallVerifiedUnder0.bpl(9,5): anon0
CallVerifiedUnder0.bpl(21,5): Error BP5002: A precondition for this call might not hold.
CallVerifiedUnder0.bpl(5,3): Related location: This is the precondition that might not hold.
Execution trace:
CallVerifiedUnder0.bpl(21,5): anon0
CallVerifiedUnder0.bpl(34,5): Error BP5002: A precondition for this call might not hold.
CallVerifiedUnder0.bpl(5,3): Related location: This is the precondition that might not hold.
Execution trace:
CallVerifiedUnder0.bpl(34,5): anon0
Boogie program verifier finished with 3 verified, 3 errors
|
