blob: edcfee63670c4d27fee0832e51a6424206a4c94f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
FreeCall.bpl(39,5): Error BP5002: A precondition for this call might not hold.
FreeCall.bpl(10,3): Related location: This is the precondition that might not hold.
Execution trace:
FreeCall.bpl(39,5): anon0
FreeCall.bpl(44,5): Error BP5002: A precondition for this call might not hold.
FreeCall.bpl(8,3): Related location: This is the precondition that might not hold.
Execution trace:
FreeCall.bpl(44,5): anon0
FreeCall.bpl(61,5): Error BP5002: A precondition for this call might not hold.
FreeCall.bpl(18,3): Related location: This is the precondition that might not hold.
Execution trace:
FreeCall.bpl(61,5): anon0
FreeCall.bpl(68,5): Error BP5002: A precondition for this call might not hold.
FreeCall.bpl(16,3): Related location: This is the precondition that might not hold.
Execution trace:
FreeCall.bpl(68,5): anon0
Boogie program verifier finished with 7 verified, 4 errors
|
