]>
Commit | Line | Data |
---|---|---|
6317f163 | 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 |