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