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