test/compdestroy.expect

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