]>
Commit | Line | Data |
---|---|---|
a469ccf0 | 1 | |
2 | buffertest1.c: (in function t1) | |
3 | buffertest1.c:5:3: Variable g used before definition | |
4 | buffertest1.c:5:3: Possible out-of-bounds store: | |
5 | Unable to resolve constraint: | |
6 | requires maxSet(g @ buffertest1.c:5:3) >= 100 | |
7 | needed to satisfy precondition: | |
8 | requires maxSet(g @ buffertest1.c:5:3) >= 100 | |
9 | buffertest1.c: (in function t2) | |
10 | buffertest1.c:20:3: Variable g used before definition | |
11 | buffertest1.c:21:3: Possible out-of-bounds store: | |
12 | Unable to resolve constraint: | |
13 | requires maxSet(g @ buffertest1.c:20:3) >= 1 | |
14 | needed to satisfy precondition: | |
15 | requires maxSet(g @ buffertest1.c:21:3) >= 0 | |
16 | buffertest1.c:21:10: Possible out-of-bounds read: | |
17 | Unable to resolve constraint: | |
18 | requires maxRead(g @ buffertest1.c:20:3) >= 2 | |
19 | needed to satisfy precondition: | |
20 | requires maxRead(g @ buffertest1.c:21:10) >= 1 | |
21 | ||
11db3170 | 22 | Finished checking --- 5 code warnings, as expected |