Properly checks struct members in alias expression

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

[martin-cs]

The code looks fairly good but I am worried about the tests and about disabling so many of them in a PR claiming to fix things.

[feliperodri]

The code looks fairly good but I am worried about the tests and about disabling so many of them in a PR claiming to fix things.

@martin-cs could you take another look? I fixed the bug when dealing with arrays.

[codecov]

Codecov Report

Merging #6265 (5daa210) into develop (dbb5163) will increase coverage by 0.00%.
The diff coverage is 97.96%.

❗ Current head 5daa210 differs from pull request most recent head 9e8dd91. Consider uploading reports for the commit 9e8dd91 to get more accurate results

@@           Coverage Diff            @@
##           develop    #6265   +/-   ##
========================================
  Coverage    75.90%   75.90%           
========================================
  Files         1492     1492           
  Lines       162724   162731    +7     
========================================
+ Hits        123513   123522    +9     
+ Misses       39211    39209    -2     

Impacted Files	Coverage Δ
jbmc/src/jdiff/jdiff_parse_options.h	100.00% <ø> (ø)
src/goto-analyzer/goto_analyzer_parse_options.cpp	71.98% <ø> (ø)
src/goto-cc/goto_cc_languages.cpp	100.00% <ø> (ø)
src/goto-diff/goto_diff_parse_options.h	100.00% <ø> (ø)
src/goto-harness/goto_harness_parse_options.cpp	68.37% <ø> (ø)
...rc/goto-instrument/goto_instrument_parse_options.h	100.00% <ø> (ø)
...rc/memory-analyzer/memory_analyzer_parse_options.h	100.00% <ø> (ø)
src/solvers/smt2_incremental/smt_sorts.cpp	94.11% <ø> (ø)
src/solvers/smt2_incremental/smt_sorts.h	100.00% <ø> (ø)
src/solvers/smt2_incremental/smt_terms.cpp	94.44% <ø> (ø)
... and 39 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 3ebacfe...9e8dd91. Read the comment docs.

[martin-cs]

Thank you; that is a massive improvement on the previous version.

[SaswatPadhi]

I am still thinking about the new conditions we have added, but my main comment for now is to add enough test cases that cover this new change.

1. We are missing test cases for replacement context. We should check that during replacement, we don't havoc more than (the struct field) we are supposed to havoc
2. Both test cases assign to the first field of the struct. Since we look at the offsets etc, could we make one of the test assign to the second field? I'd suggest changing regression/contracts/assigns_enforce_structs_04/main.c to assign to p->y instead.

[feliperodri]

1. We are missing test cases for replacement context. We should check that during replacement, we don't havoc more than (the struct field) we are supposed to havoc

This PR is only for enforcement. We should add test cases for replacement once we update the havoc method.

2. Both test cases assign to the first field of the struct. Since we look at the offsets etc, could we make one of the test assign to the second field? I'd suggest changing `regression/contracts/assigns_enforce_structs_04/main.c` to assign to `p->y` instead.

I added two new test cases, could you take another look? @SaswatPadhi

[SaswatPadhi]

Thanks, LGTM. If you rebase on to develop, you could remove some repeated code. Commented below: