]>
Commit | Line | Data |
---|---|---|
1 | ||
2 | unrecogCall.c: (in function foo) | |
3 | unrecogCall.c:8:3: Unrecognized identifier: bar | |
4 | initialization.c: (in function initialization) | |
5 | initialization.c:5:10: Variable g declared but not used | |
6 | initialization.c:5:14: Possible out-of-bounds read: | |
7 | e[22] | |
8 | Unable to resolve constraint: | |
9 | requires maxRead(d @ initialization.c:3:14) >= 22 | |
10 | needed to satisfy precondition: | |
11 | requires maxRead(e @ initialization.c:5:14) >= 22 | |
12 | initialization.c:8:3: Possible out-of-bounds store: | |
13 | f[2] | |
14 | Unable to resolve constraint: | |
15 | requires maxSet(d @ initialization.c:3:14) >= 2 | |
16 | needed to satisfy precondition: | |
17 | requires maxSet(f @ initialization.c:8:3) >= 2 | |
18 | simplifyTest.c: (in function fooSub) | |
19 | simplifyTest.c:3:3: Possible out-of-bounds store: | |
20 | s[i] | |
21 | Unable to resolve constraint: | |
22 | requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5 | |
23 | needed to satisfy precondition: | |
24 | requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5 | |
25 | simplifyTest.c: (in function fooAdd) | |
26 | simplifyTest.c:10:3: Possible out-of-bounds store: | |
27 | s[i + 2] | |
28 | Unable to resolve constraint: | |
29 | requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2 | |
30 | needed to satisfy precondition: | |
31 | requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2 | |
32 | strncatNotReallyGood.c: (in function NotGoodfunc) | |
33 | strncatNotReallyGood.c:4:29: Passed storage buffer not completely defined | |
34 | (*buffer is undefined): strncat (buffer, ...) | |
35 | strncatNotReallyGood.c:4:21: Possible out-of-bounds store: | |
36 | strncat(buffer, str, sizeof((buffer)) - 1) | |
37 | Unable to resolve constraint: | |
38 | requires maxRead(buffer @ strncatNotReallyGood.c:4:29) <= 0 | |
39 | needed to satisfy precondition: | |
40 | requires maxSet(buffer @ strncatNotReallyGood.c:4:29) >= maxRead(buffer @ | |
41 | strncatNotReallyGood.c:4:29) + 255 | |
42 | derived from strncat precondition: requires maxSet(<parameter 1>) >= | |
43 | maxRead(<parameter 1>) + <parameter 3> | |
44 | ||
45 | Finished checking --- 8 code warnings, as expected |