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