test/mystrncat.expect

   1
   2 mystrncat.c: (in function func)
   3 mystrncat.c:12:13: Passed storage buffer not completely defined (*buffer is
   4                       undefined): mystrncat (buffer, ...)
   5 mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined):
   6                       mystrncat (b, ...)
   7    mystrncat.c:10:3: Storage *b allocated
   8 mystrncat.c:12:3: Possible out-of-bounds store:
   9     mystrncat(buffer, str, sizeof((buffer)) - 1)
  10     Unable to resolve constraint:
  11     requires maxRead(buffer @ mystrncat.c:12:13) <= 0
  12      needed to satisfy precondition:
  13     requires maxSet(buffer @ mystrncat.c:12:13) >= maxRead(buffer @
  14     mystrncat.c:12:13) + 255
  15      derived from mystrncat precondition:
  16     requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
  17 mystrncat.c:13:3: Possible out-of-bounds store:
  18     mystrncat(b, str, sizeof((buffer)) - 1)
  19     Unable to resolve constraint:
  20     requires maxRead(malloc(256) @ mystrncat.c:10:7) <= 0
  21      needed to satisfy precondition:
  22     requires maxSet(b @ mystrncat.c:13:13) >= maxRead(b @ mystrncat.c:13:13) +
  23     255
  24      derived from mystrncat precondition:
  25     requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
  26
  27 Finished checking --- 4 code warnings, as expected