Handle loop contracts on do/while loops

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

Currently do/while loops are not handled correctly in the contracts instrumentation pass.

The tricky bit here is the first unguarded iteration. It's syntactically "inside" the loop, but the "base case" assertion must be placed after it, which might be confusing to users.