1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
compdestroy.c: (in function sip_free2)
compdestroy.c:25:9: Only storage *(x->ips) (type oip) derived from released
storage is not released (memory leak): x->ips
Finished checking --- 1 code warning, as expected
compdestroy.c: (in function sip_free)
compdestroy.c:19:9: Only storage x->ips[] (type oip) derived from released
storage may not have been released: x->ips
compdestroy.c: (in function sip_free2)
compdestroy.c:25:9: Only storage *(x->ips) (type oip) derived from released
storage is not released (memory leak): x->ips
Finished checking --- 2 code warnings, as expected
compdestroy.c: (in function sip_free)
compdestroy.c:16:13: Possibly dead storage x->ips[] passed as out parameter:
x->ips[i]
compdestroy.c:15:13: Storage x->ips[] possibly released
compdestroy.c:19:9: Only storage x->ips[] (type oip) derived from released
storage may not have been released: x->ips
compdestroy.c: (in function sip_free2)
compdestroy.c:25:9: Only storage *(x->ips) (type oip) derived from released
storage is not released (memory leak): x->ips
Finished checking --- 3 code warnings, as expected
compdestroy.c: (in function sip_free)
compdestroy.c:16:13: Possibly dead storage x->ips[] passed as out parameter:
x->ips[i]
compdestroy.c:15:13: Storage x->ips[] possibly released
compdestroy.c:19:9: Only storage x->ips[] (type oip) derived from released
storage may not have been released: x->ips
compdestroy.c:15:13: Possible out-of-bounds read: x->ips[i]
Unable to resolve constraint:
requires maxRead(x->ips @ compdestroy.c:15:13) >= i @ compdestroy.c:15:20
needed to satisfy precondition:
requires maxRead(x->ips @ compdestroy.c:15:13) >= i @ compdestroy.c:15:20
compdestroy.c: (in function sip_free2)
compdestroy.c:25:9: Only storage *(x->ips) (type oip) derived from released
storage is not released (memory leak): x->ips
Finished checking --- 4 code warnings, as expected
|
