Propagate write-set checks to sub-functions

[feliperodri]

• 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 #6371 (3f48b6e) into develop (eebdba8) will decrease coverage by 0.00%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #6371      +/-   ##
===========================================
- Coverage    75.91%   75.90%   -0.01%     
===========================================
  Files         1517     1517              
  Lines       164022   163893     -129     
===========================================
- Hits        124513   124406     -107     
+ Misses       39509    39487      -22     

Impacted Files	Coverage Δ
src/ansi-c/expr2c.cpp	65.34% <ø> (+0.07%)	⬆️
src/goto-instrument/contracts/assigns.h	100.00% <ø> (ø)
src/goto-instrument/contracts/contracts.h	100.00% <ø> (ø)
...rc/goto-instrument/goto_instrument_parse_options.h	100.00% <ø> (ø)
src/ansi-c/ansi_c_convert_type.cpp	78.98% <100.00%> (-0.31%)	⬇️
src/ansi-c/ansi_c_convert_type.h	100.00% <100.00%> (ø)
src/ansi-c/c_typecheck_base.cpp	78.76% <100.00%> (+0.34%)	⬆️
src/goto-instrument/contracts/assigns.cpp	98.43% <100.00%> (+1.84%)	⬆️
src/goto-instrument/contracts/contracts.cpp	95.77% <100.00%> (+1.02%)	⬆️
.../goto-instrument/goto_instrument_parse_options.cpp	68.29% <100.00%> (-0.01%)	⬇️
... and 6 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 1ab9590...3f48b6e. Read the comment docs.

[SaswatPadhi]

Thanks! That's quite a lot of cleanup and fixes.

I have a few minor comments and only major comments about subset check part.

[SaswatPadhi]

LGTM. Thanks!

[SaswatPadhi]

One minor comment: We have many tiny commits in this PR and could merge some of these together (especially if they are related) for a cleaner history. For example 77b2d94 and d5374d7 could definitely be merged together.

[martin-cs]

I am approving this because 1. I do not see any blocking problems here, 2. as far as I know you are the main users of this code so changes in the functionality & interface are not likely to affect others too much and 3. I know it is urgent for you. But, I found this quite hard to review. In the future, if you have the time please could you consider:

1. Smaller PRs -- this does a number of related, but different things and would be easier to review in chunks.
2. A description of what you are doing and why in each commit message. They are one line at the moment which is better than nothing but it gives more limited context.
3. More of a over-view description in the PR.

[martin-cs]

I am a little concerned by the change in functionality. I realise that it would be good to have the extra flexibility but having to give a command-line argument for every function is quite a lot. Elsewhere I have seen regexes used for this kind of thing.

[feliperodri]

We we're using contracts now in a context where an user enforces one contract at a time, makes sure it is correct and then uses it during replacement. In the future, we still want to have an option where we can simply apply contracts whenever they are available, but for now we want to force users to specify which contracts must be enforced or replaced.

[feliperodri]

I am approving this because 1. I do not see any blocking problems here, 2. as far as I know you are the main users of this code so changes in the functionality & interface are not likely to affect others too much and 3. I know it is urgent for you. But, I found this quite hard to review. In the future, if you have the time please could you consider:

1. Smaller PRs -- this does a number of related, but different things and would be easier to review in chunks.

2. A description of what you are doing and why in each commit message.  They are one line at the moment which is better than nothing but it gives more limited context.

3. More of a over-view description in the PR.

Thanks for the review @martin-cs. I'll at least add a better description for this PR now (3) and keep in mind (1) and (2) for future PRs.