test/moreBufferTests.expect

   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