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