requires maxRead(buffer @ mystrncat.c:12:13) <= 0
needed to satisfy precondition:
requires maxSet(buffer @ mystrncat.c:12:13) >= maxRead(buffer @
mystrncat.c:12:13) + 255
derived from mystrncat precondition:
requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>
requires maxRead(buffer @ mystrncat.c:12:13) <= 0
needed to satisfy precondition:
requires maxSet(buffer @ mystrncat.c:12:13) >= maxRead(buffer @
mystrncat.c:12:13) + 255
derived from mystrncat precondition:
requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3>