test/constannot.expect

   1
   2 constannot.c: (in function foo2)
   3 constannot.c:11:3: Possible out-of-bounds store: str[20]
   4     Unable to resolve constraint:
   5     requires maxSet(str @ constannot.c:11:3) >= 20
   6      needed to satisfy precondition:
   7     requires maxSet(str @ constannot.c:11:3) >= 20
   8 constannot.c: (in function foo3)
   9 constannot.c:20:3: Likely out-of-bounds store: foo(buf)
  10     Unable to resolve constraint:
  11     requires <const int=20> <= 19
  12      needed to satisfy precondition:
  13     requires maxSet(buf @ constannot.c:20:8) >= <const int=20>
  14      derived from foo precondition: requires maxSet(<parameter 1>) >= <const
  15     int=20>
  16
  17 Finished checking --- 2 code warnings, as expected