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