+
+malloc.c: (in function f1)
+malloc.c:3:21: Allocated memory is converted to type int * of (size 32), which
+ is not divisible into original allocation of space for 89 elements of type
+ void * (size 8)
+malloc.c:5:5: Likely out-of-bounds store: ip[88]
+ Unable to resolve constraint:
+ requires 21 >= 88
+ needed to satisfy precondition:
+ requires maxSet(ip @ malloc.c:5:5) >= 88
+malloc.c: (in function f2)
+malloc.c:15:5: Likely out-of-bounds store: ip[22]
+ Unable to resolve constraint:
+ requires 21 >= 22
+ needed to satisfy precondition:
+ requires maxSet(ip @ malloc.c:15:5) >= 22
+malloc.c: (in function f3)
+malloc.c:26:5: Likely out-of-bounds store: ip[87]
+ Unable to resolve constraint:
+ requires 86 >= 87
+ needed to satisfy precondition:
+ requires maxSet(ip @ malloc.c:26:5) >= 87
+malloc.c: (in function f4)
+malloc.c:33:21: Allocated memory is used as a different type (int) from the
+ sizeof type (short int)
+malloc.c:33:21: Allocated memory is converted to type int * of (size 32), which
+ is not divisible into original allocation of space for 87 elements of type
+ short int (size 8)
+malloc.c:35:5: Likely out-of-bounds store: ip[86]
+ Unable to resolve constraint:
+ requires 20 >= 86
+ needed to satisfy precondition:
+ requires maxSet(ip @ malloc.c:35:5) >= 86
+
+Finished checking --- 7 code warnings, as expected