]>
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: |
9276a168 | 7 | e[22] |
7bf96067 | 8 | Unable to resolve constraint: |
4109ede4 | 9 | requires maxRead(d @ initialization.c:3:14) >= 22 |
03d670b6 | 10 | needed to satisfy precondition: |
4109ede4 | 11 | requires maxRead(e @ initialization.c:5:14) >= 22 |
7bf96067 | 12 | initialization.c:8:3: Possible out-of-bounds store: |
9276a168 | 13 | f[2] |
7bf96067 | 14 | Unable to resolve constraint: |
bf5819c8 | 15 | requires maxSet(d @ initialization.c:3:14) >= 2 |
16 | needed to satisfy precondition: | |
17 | requires maxSet(f @ initialization.c:8:3) >= 2 | |
dcf136ce | 18 | simplifyTest.c: (in function fooSub) |
7bf96067 | 19 | simplifyTest.c:3:3: Possible out-of-bounds store: |
9276a168 | 20 | s[i] |
7bf96067 | 21 | Unable to resolve constraint: |
4109ede4 | 22 | requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5 |
03d670b6 | 23 | needed to satisfy precondition: |
4109ede4 | 24 | requires maxSet(s @ simplifyTest.c:3:3) >= i @ simplifyTest.c:3:5 |
dcf136ce | 25 | simplifyTest.c: (in function fooAdd) |
7bf96067 | 26 | simplifyTest.c:10:3: Possible out-of-bounds store: |
9276a168 | 27 | s[i + 2] |
7bf96067 | 28 | Unable to resolve constraint: |
4109ede4 | 29 | requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2 |
03d670b6 | 30 | needed to satisfy precondition: |
4109ede4 | 31 | requires maxSet(s @ simplifyTest.c:10:3) >= i @ simplifyTest.c:10:5 + 2 |
6e5d6478 | 32 | strncatNotReallyGood.c: (in function NotGoodfunc) |
33 | strncatNotReallyGood.c:4:29: Passed storage buffer not completely defined | |
34 | (*buffer is undefined): strncat (buffer, ...) | |
7bf96067 | 35 | strncatNotReallyGood.c:4:21: Possible out-of-bounds store: |
9276a168 | 36 | strncat(buffer, str, sizeof((buffer)) - 1) |
7bf96067 | 37 | Unable to resolve constraint: |
4109ede4 | 38 | requires maxRead(buffer @ strncatNotReallyGood.c:4:29) <= 0 |
03d670b6 | 39 | needed to satisfy precondition: |
4109ede4 | 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> | |
80ee600a | 44 | |
11db3170 | 45 | Finished checking --- 8 code warnings, as expected |