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