Before, some temporary variables were declared to point to various positions in a string. These variables were safely accessed after a length check passed. Newer versions of CBMC flag this as a possible issue. This PR moves the declarations after the length check and the proof runs cleanly again.
Before, some temporary variables were declared to point to various positions in a string. These variables were safely accessed after a length check passed. Newer versions of CBMC flag this as a possible issue. This PR moves the declarations after the length check and the proof runs cleanly again.