test/malloc.expect

   1
   2 malloc.c: (in function f1)
   3 malloc.c:3:21: Allocated memory is converted to type int * of (size 32), which
   4     is not divisible into original allocation of space for 89 elements of type
   5     void * (size 8)
   6 malloc.c:5:5: Likely out-of-bounds store: ip[88]
   7     Unable to resolve constraint:
   8     requires 21 >= 88
   9      needed to satisfy precondition:
  10     requires maxSet(ip @ malloc.c:5:5) >= 88
  11 malloc.c: (in function f2)
  12 malloc.c:15:5: Likely out-of-bounds store: ip[22]
  13     Unable to resolve constraint:
  14     requires 21 >= 22
  15      needed to satisfy precondition:
  16     requires maxSet(ip @ malloc.c:15:5) >= 22
  17 malloc.c: (in function f3)
  18 malloc.c:26:5: Likely out-of-bounds store: ip[87]
  19     Unable to resolve constraint:
  20     requires 86 >= 87
  21      needed to satisfy precondition:
  22     requires maxSet(ip @ malloc.c:26:5) >= 87
  23 malloc.c: (in function f4)
  24 malloc.c:33:21: Allocated memory is used as a different type (int) from the
  25                    sizeof type (short int)
  26 malloc.c:33:21: Allocated memory is converted to type int * of (size 32), which
  27     is not divisible into original allocation of space for 87 elements of type
  28     short int (size 8)
  29 malloc.c:35:5: Likely out-of-bounds store: ip[86]
  30     Unable to resolve constraint:
  31     requires 20 >= 86
  32      needed to satisfy precondition:
  33     requires maxSet(ip @ malloc.c:35:5) >= 86
  34
  35 Finished checking --- 7 code warnings, as expected