CONTRACTS: fix do while latch

[remi-delmas-3000]

Ensures that loop normalization for contracts rewrites latches into unconditional jumps.
In particular, latch nodes for do-while loops go from

preamble();
do
__CPROVER_assigns(A)
__CPROVER_loop_invariant(I)
__CPROVER_decreases(D)
{
body();
} while(cond);
postamble();

gets normalized to

  preamble();
head:
  body();
  if !cond GOTO exit;
  if true {C_spec_assigns :A, C_spec_loop_invariant:I, C_spec_decreases: D} GOTO head;
exit:
  postamble();

contract clauses are attached to the unconditional latch node.

• Each commit message has a non-empty body, explaining why the change was made.
  doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Attention: Patch coverage is 80.00000% with 3 lines in your changes missing coverage. Please review.

Project coverage is 77.85%. Comparing base (dae5af0) to head (159abec).
Report is 2 commits behind head on develop.

Files	Patch %	Lines
...cts/dynamic-frames/dfcc_check_loop_normal_form.cpp	80.00%	3 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8420      +/-   ##
===========================================
- Coverage    77.85%   77.85%   -0.01%     
===========================================
  Files         1726     1726              
  Lines       189886   189899      +13     
  Branches     18223    18225       +2     
===========================================
+ Hits        147835   147844       +9     
- Misses       42051    42055       +4     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[qinheping]

LGTM