CONTRACTS: Dynamic frames for loop contracts

[qinheping]

This PR adds support for loop contracts with dynamic frames.

The first two commits are from #7671 #7672, please review separately.

Fixes #7196
Fixes #7517

We modify the dfcc_instrument class to use dfcc_instrument_loopt and apply loop contracts transformation at the same time as dynamic frame instrumentation, when the --apply-loop-contract-flag is set.

We also port the tests from the previous loop contracts implementation to the new one, and add some tests that combine loop contracts and recursive functions.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in 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 commit message includes data points confirming performance improvements (if claimed).
• 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

Patch coverage: 90.64% and project coverage change: +0.04 🎉

Comparison is base (521fa25) 78.50% compared to head (56bf6c1) 78.55%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7541      +/-   ##
===========================================
+ Coverage    78.50%   78.55%   +0.04%     
===========================================
  Files         1674     1686      +12     
  Lines       191955   192915     +960     
===========================================
+ Hits        150699   151539     +840     
- Misses       41256    41376     +120     

Impacted Files	Coverage Δ
...cts/dynamic-frames/dfcc_contract_clauses_codegen.h	100.00% <ø> (+100.00%)	⬆️
...contracts/dynamic-frames/dfcc_contract_functions.h	100.00% <ø> (ø)
...rument/contracts/dynamic-frames/dfcc_is_freeable.h	100.00% <ø> (ø)
...nstrument/contracts/dynamic-frames/dfcc_is_fresh.h	100.00% <ø> (ø)
...cts/dynamic-frames/dfcc_lift_memory_predicates.cpp	89.50% <ø> (ø)
...ent/contracts/dynamic-frames/dfcc_obeys_contract.h	100.00% <ø> (ø)
...t/contracts/dynamic-frames/dfcc_pointer_in_range.h	100.00% <ø> (ø)
...ent/contracts/dynamic-frames/dfcc_spec_functions.h	100.00% <ø> (+100.00%)	⬆️
...ment/contracts/dynamic-frames/dfcc_swap_and_wrap.h	100.00% <ø> (+16.66%)	⬆️
...nt/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp	83.47% <13.33%> (-2.89%)	⬇️
... and 12 more

... and 23 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

[remi-delmas-3000]

Please apply the script from the commit message in 01fd5ea to de-duplicate tests.

Deduplication done

[tautschnig]

Seems ok to me except for the spurious debug file.

[feliperodri]

LGTM modulo Michael's comments.