unrecogCall.c:8:3: Unrecognized identifier: bar
initialization.c: (in function initialization)
initialization.c:5:10: Variable g declared but not used
-initialization.c:8:3: Possible out-of-bounds store. Unable to resolve
- constraint:
- requires: : maxSet ((d @ initialization.c:3:14 ) ) >= ( 2 )
+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: : maxSet ((f @ initialization.c:8:3 ) ) >= ( 2 )
-initialization.c:5:14: Possible out-of-bounds read. Unable to resolve
- constraint:
- requires: : maxRead ((d @ initialization.c:3:14 ) ) >= ( 22 )
+ 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: : maxRead ((e @ initialization.c:5:14 ) ) >= ( 22 )
+ requires maxSet(f @ initialization.c:8:3) >= 2
simplifyTest.c: (in function fooSub)
-simplifyTest.c:3:3: Possible out-of-bounds store. Unable to resolve
- constraint:
- requires: : maxSet ((s @ simplifyTest.c:3:3 ) ) >= (i @
- simplifyTest.c:3:5 )
+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 )
+ 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. Unable to resolve
- constraint:
- requires: : maxSet ((s @ simplifyTest.c:10:3 ) ) >= ((i @
- simplifyTest.c:10:5 ) ) + (( 2 ) )
+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 ) )
+ 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. Unable to resolve
- constraint:
- requires: : maxRead ((buffer @ strncatNotReallyGood.c:4:29 ) ) <= ( 0 )
+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> ) )
+ 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 LCLint checking --- 8 code errors found
+Finished checking --- 8 code warnings, as expected