]>
Commit | Line | Data |
---|---|---|
30585c35 | 1 | |
2 | unknownsize.c: (in function uknSize1) | |
6317f163 | 3 | unknownsize.c:9:3: Possible out-of-bounds store: c[9] |
30585c35 | 4 | Unable to resolve constraint: |
5 | requires maxSet(c @ unknownsize.c:9:3) >= 9 | |
6 | needed to satisfy precondition: | |
7 | requires maxSet(c @ unknownsize.c:9:3) >= 9 | |
8 | ||
a956d444 | 9 | Finished checking --- 1 code warning, as expected |
e7af8598 | 10 | |
11 | fixedArrayType.c: (in function fixedArrayTouch) | |
6317f163 | 12 | fixedArrayType.c:9:3: Possible out-of-bounds store: buffer[sizeof(Array) - 1] |
e7af8598 | 13 | Unable to resolve constraint: |
abd7f895 | 14 | requires sizeof(Array) @ fixedArrayType.c:9:25 <= 10 |
e7af8598 | 15 | needed to satisfy precondition: |
16 | requires maxSet(buffer @ fixedArrayType.c:9:3) >= sizeof(Array) @ | |
abd7f895 | 17 | fixedArrayType.c:9:25 - 1 |
e7af8598 | 18 | |
19 | Finished checking --- 1 code warning, as expected | |
8f58355a | 20 | |
21 | initBlock.c: (in function main) | |
22 | initBlock.c:8:3: Likely out-of-bounds store: buf[10] | |
23 | Unable to resolve constraint: | |
24 | requires 9 >= 10 | |
25 | needed to satisfy precondition: | |
26 | requires maxSet(buf @ initBlock.c:8:3) >= 10 | |
27 | ||
28 | Finished checking --- 1 code warning, as expected |