test/maxset.expect

   1
   2 Finished checking --- no warnings
   3
   4 maxsetnoannotations.c: (in function noancopy)
   5 maxsetnoannotations.c:2:3: Possible out-of-bounds store:
   6     strcpy(a, b)
   7     Unable to resolve constraint:
   8     requires maxSet(a @ maxsetnoannotations.c:2:11) >= maxRead(b @
   9     maxsetnoannotations.c:2:13)
  10      needed to satisfy precondition:
  11     requires maxSet(a @ maxsetnoannotations.c:2:11) >= maxRead(b @
  12     maxsetnoannotations.c:2:13)
  13      derived from strcpy precondition: requires maxSet(<parameter 1>) >=
  14     maxRead(<parameter 2>)
  15
  16 Finished checking --- 1 code warning, as expected