Supports history variables in function contracts

[ArenBabikian]

This PR adds support for history variables in __CPROVER_ensures contracts. Specifically, users may now access the pre-function call state of a variable within the post-condition.

Let us consider the following example. Semantically, this example shows a case where the post-condition of a function call ensures that ( the post-call value of x ) is greater than ( the pre-call value of x + 2 ).

void foo(int *x) __CPROVER_assigns(*x)
  __CPROVER_requires(*x > 0)
  __CPROVER_ensures(*x > __CPROVER_old(*x) + 2)
{
  *x = *x + 2;
}

In this case, the variable that we are interested in is x, which is modified by the call to foo(int *x). The pre-condition contract (__CPROVER_requires) may only access the pre-state of the variable x (this is done through the inclusion of *x). However, the post-condition (__CPROVER_ensures) accesses both the post-state of x (through *x) and the pre-state of x (through __CPROVER_old(*x))

Note:
We currently only support pointers within the __CPROVER_old() construct. In the near future, we plan to add support for symbols and struct members.

---

• 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 #6025 (e5d7738) into develop (535dc20) will decrease coverage by 1.46%.
The diff coverage is 94.59%.

❗ Current head e5d7738 differs from pull request most recent head 6ce96c7. Consider uploading reports for the commit 6ce96c7 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6025      +/-   ##
===========================================
- Coverage    75.68%   74.22%   -1.47%     
===========================================
  Files         1447     1446       -1     
  Lines       157837   157540     -297     
===========================================
- Hits        119465   116936    -2529     
- Misses       38372    40604    +2232     

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_base.cpp	53.84% <0.00%> (-24.40%)	⬇️
src/ansi-c/c_typecheck_base.h	100.00% <ø> (ø)
src/goto-instrument/code_contracts.h	94.11% <ø> (ø)
src/ansi-c/c_typecheck_expr.cpp	75.41% <85.00%> (+0.71%)	⬆️
src/goto-instrument/code_contracts.cpp	85.32% <100.00%> (+0.57%)	⬆️
src/util/ghost_variables.h	100.00% <100.00%> (ø)
src/goto-instrument/wmm/shared_buffers.h	0.00% <0.00%> (-95.24%)	⬇️
src/goto-checker/goto_symex_fault_localizer.cpp	0.00% <0.00%> (-82.46%)	⬇️
src/goto-programs/link_goto_model.cpp	0.00% <0.00%> (-77.97%)	⬇️
src/goto-instrument/wmm/shared_buffers.cpp	0.00% <0.00%> (-77.84%)	⬇️
... and 702 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 ffd4ccf...6ce96c7. Read the comment docs.

[SaswatPadhi]

The PR overall looks good. I list several comments regarding simplifying the code and clarifying the regression tests.

One meta comment about regression tests: you only check for exit code and verification success and failure. Could you please also add some regexes in the test.desc files to check if the contracts are actually being processed? They must be generating some additional assertions, for which we should have regexes.

[SaswatPadhi]

The regexes you added to test.desc files look good and now we're checking that contracts are actually working as expected.

I have only 2 comments:

[SaswatPadhi]

LGTM! Thanks for all the changes.

[feliperodri]

LGTM.

[feliperodri]

Hi @kroening @tautschnig could you review this PR? It's missing code owner approval.

[kroening]

While it's conceivable that other languages may eventually offer a similar mechanism, may I suggest to add old_exprt to ansi-c/c_expr.h for now.

[ArenBabikian]

@kroening Thanks for the comment, I have made the required changes.