1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
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
|
