[CONTRACTS] Use unified loop contract config

[qinheping]

We now use boolean flag for old loop contracts and dfcc_loop_contract_mode for dfcc loop contracts to manage the configuration of loop contracts, which is hard to extend.

This PR will add a new struct loop_contract_config to manage config for both loop contracts.

• 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.

[feliperodri]

I'm a little concern about this. Why would users need to unwind loop at least twice? The advice should be they must unwind the loops to pass unwinding assertions. Also, this option is not set by default, correct? Why is this Kani specific? Maybe we should re-phrase the documentation to be more general. For instance, I don't see a problem for us to require users to unwind the the remaining loops after loop contract instrumentation, maybe we can even report to them the remaining loops, we don't need to justify this by Kani since it's only a user of the feature, right?

[tautschnig]

Although this is just code moved around in this PR I'm with Felipe that this PR is an opportunity to improve on the documentation.

[qinheping]

After the instrumentation, the transformed will contains a back jump. Running CBMC with unwinding bound 1 will fail the unwinding assertions. Not providing unwinding bounds or providing bounds greater than 1 are fine.

By default, goto-instrument will unwinding the instrumented loops by 2.

It is not Kani specific. I will update the documentation and clarify the motivation of this flag.

[tautschnig]

Although this is just code moved around in this PR I'm with Felipe that this PR is an opportunity to improve on the documentation.

[codecov]

Codecov Report

Attention: Patch coverage is 56.14035% with 25 lines in your changes missing coverage. Please review.

Project coverage is 78.27%. Comparing base (2ffc4c9) to head (a7afbe2).
Report is 12 commits behind head on develop.

Files	Patch %	Lines
...c/goto-instrument/contracts/loop_contract_config.h	0.00%	9 Missing ⚠️
...nt/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp	12.50%	7 Missing ⚠️
.../goto-instrument/goto_instrument_parse_options.cpp	73.33%	4 Missing ⚠️
src/goto-instrument/contracts/contracts.h	40.00%	3 Missing ⚠️
...ument/contracts/dynamic-frames/dfcc_instrument.cpp	75.00%	1 Missing ⚠️
...oto-synthesizer/goto_synthesizer_parse_options.cpp	80.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8356      +/-   ##
===========================================
+ Coverage    78.09%   78.27%   +0.17%     
===========================================
  Files         1726     1726              
  Lines       189039   188605     -434     
  Branches     18399    18443      +44     
===========================================
  Hits        147629   147629              
+ Misses       41410    40976     -434     

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