Simplify the annotations on strlen()

This improves verification speed and allows additional vcc invocations to
be uncommented (previously the verifier would either stall or run out of
memory).
Remove a limitation on strcat()

Previously it was required that b[b_nul_pos + str_nul_pos] == '\0'. This
was to make sure that strlen(b, b_nul_pos + str_nul_pos) was well-defined.