blob: 5d407874e05f08990c33af6da72c7e2e6a9250cc (
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
|
