]>
Commit | Line | Data |
---|---|---|
1 | ||
2 | m.c: (in function t) | |
3 | m.c:9:1: Index of possibly null pointer f: f | |
4 | m.c:8:5: Storage f may become null | |
5 | sizeof.c: (in function f) | |
6 | sizeof.c:17:1: Likely out-of-bounds store: x[(sizeof(x))] | |
7 | Unable to resolve constraint: | |
8 | requires 2 >= 3 | |
9 | needed to satisfy precondition: | |
10 | requires maxSet(x @ sizeof.c:17:1) >= 3 | |
11 | test3.c:2:6: Function t defined more than once | |
12 | m.c:11:1: Previous definition of t | |
13 | test3.c: (in function t) | |
14 | test3.c:9:3: Likely out-of-bounds store: g[101] | |
15 | Unable to resolve constraint: | |
16 | requires 99 >= 101 | |
17 | needed to satisfy precondition: | |
18 | requires maxSet(g @ test3.c:9:3) >= 101 | |
19 | test7.c:2:6: Function t defined more than once | |
20 | m.c:11:1: Previous definition of t | |
21 | test7.c: (in function t) | |
22 | test7.c:6:3: Possible out-of-bounds store: g[2] | |
23 | Unable to resolve constraint: | |
24 | requires maxSet(g @ test7.c:4:3) >= 4 | |
25 | needed to satisfy precondition: | |
26 | requires maxSet(g @ test7.c:6:3) >= 2 | |
27 | test7.c:8:3: Possible out-of-bounds store: j[0] | |
28 | Unable to resolve constraint: | |
29 | requires maxSet(j @ test7.c:8:3) >= 0 | |
30 | needed to satisfy precondition: | |
31 | requires maxSet(j @ test7.c:8:3) >= 0 | |
32 | ||
33 | Finished checking --- 7 code warnings, as expected |