]>
Commit | Line | Data |
---|---|---|
1 | ||
2 | unknownsize.c: (in function uknSize1) | |
3 | unknownsize.c:9:3: Possible out-of-bounds store: c[9] | |
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 | ||
9 | Finished checking --- 1 code warning, as expected | |
10 | ||
11 | fixedArrayType.c: (in function fixedArrayTouch) | |
12 | fixedArrayType.c:9:3: Possible out-of-bounds store: buffer[sizeof(Array) - 1] | |
13 | Unable to resolve constraint: | |
14 | requires sizeof(Array) @ fixedArrayType.c:9:25 <= 10 | |
15 | needed to satisfy precondition: | |
16 | requires maxSet(buffer @ fixedArrayType.c:9:3) >= sizeof(Array) @ | |
17 | fixedArrayType.c:9:25 - 1 | |
18 | ||
19 | Finished checking --- 1 code warning, as expected |