Invalid dereference in loops termination benchmark

[xvitovs1]

There can be an invalid dereference in benchmark loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i on line 61 which leads to undefined behavior.

The benchmark is labeled as false-unreach-call, which means that the assertion __VERIFIER_assert(j - start + 1 < 2) can fail. In that case, the call on the previous line to strncpy(str2, str+start, j-start+1) leads to invalid dereference, as str2 is an array of size 2.

[danieldietsch]

Note: this is a sideeffect from the conversion of r_strncpy from an undefined function to the actual function.