CONTRACTS: Moving check_frame_conditions to instrument_assigns_clauset.

[remi-delmas-3000]

To further encapsulate the the assigns clause checking algorithm in instrument_assigns_clause.cpp

• the check_frame_conditions method and related functions have been moved from contracts.cpp and utils.cpp to instrument_assigns_clause.cpp.
• the former track_static_locals method is now available in two different versions:
  • track_static_locals(dest) which tracks all local static variables touched directly or indirectly by the whole instrumented function (for function contracts)
  • track_static_locals_from_calls(begin, end, dest) which tracks all local static variables declared by functions that are called between the begin and end instructions (for loop contracts).

No functionality or performance impact expected.

• 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

Merging #6643 (75ea974) into develop (53c53f3) will increase coverage by 0.02%.
The diff coverage is 98.64%.

❗ Current head 75ea974 differs from pull request most recent head 222d266. Consider uploading reports for the commit 222d266 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6643      +/-   ##
===========================================
+ Coverage    76.79%   76.82%   +0.02%     
===========================================
  Files         1582     1582              
  Lines       182600   182767     +167     
===========================================
+ Hits        140231   140403     +172     
+ Misses       42369    42364       -5     

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	100.00% <ø> (ø)
...oto-instrument/contracts/instrument_spec_assigns.h	100.00% <ø> (ø)
src/goto-instrument/contracts/utils.cpp	89.24% <ø> (+3.65%)	⬆️
src/goto-instrument/contracts/utils.h	100.00% <ø> (ø)
src/util/pointer_offset_size.cpp	92.52% <ø> (ø)
src/ansi-c/expr2c.cpp	66.24% <93.10%> (ø)
src/goto-instrument/contracts/contracts.cpp	89.22% <100.00%> (-1.53%)	⬇️
...o-instrument/contracts/instrument_spec_assigns.cpp	96.86% <100.00%> (+1.50%)	⬆️
src/ansi-c/c_typecheck_expr.cpp	76.45% <0.00%> (-0.15%)	⬇️
... and 7 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 1fd7a56...222d266. Read the comment docs.

[feliperodri]

Only a few clarifications before approval.

[feliperodri]

* the `check_frame_conditions` method and related functions have been moved from `contracts.cpp` and `utils.cpp` to `instrument_assigns_clause.cpp`.

* the former `track_static_locals` method is now available in two different versions:
  
  * `track_static_locals_whole_function(dest)` which tracks all local static variables touched directly or indirectly by the whole instrumented function (for function contracts)
  * `track_static_locals_in_range(begin, end, dest)` which tracks all local static variables touched by function calls found between the begin and end instructions (for loop contracts).

@remi-delmas-3000 I'd create one commit for each one of these two main bullet points.

[remi-delmas-3000]

I addressed all comments, removed dead code, and removed the changes to local static detection. I think it is stable now.