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