test/buffertest.expect

   1
   2 buffertest1.c: (in function t1)
   3 buffertest1.c:5:3: Variable g used before definition
   4 buffertest1.c:5:3: Possible out-of-bounds store:
   5     Unable to resolve constraint:
   6     requires maxSet(g @ buffertest1.c:5:3) >= 100
   7      needed to satisfy precondition:
   8     requires maxSet(g @ buffertest1.c:5:3) >= 100
   9 buffertest1.c: (in function t2)
  10 buffertest1.c:20:3: Variable g used before definition
  11 buffertest1.c:21:3: Possible out-of-bounds store:
  12     Unable to resolve constraint:
  13     requires maxSet(g @ buffertest1.c:20:3) >= 1
  14      needed to satisfy precondition:
  15     requires maxSet(g @ buffertest1.c:21:3) >= 0
  16 buffertest1.c:21:10: Possible out-of-bounds read:
  17     Unable to resolve constraint:
  18     requires maxRead(g @ buffertest1.c:20:3) >= 2
  19      needed to satisfy precondition:
  20     requires maxRead(g @ buffertest1.c:21:10) >= 1
  21
  22 Finished checking --- 5 code warnings, as expected