Adds support for function calls within contracts

[feliperodri]

Contracts definitions often makes use of elaborate predicates,
which could be written on a separate functions. Therefore,
function contracts should be able to accept functions
as part of their specifications.

Signed-off-by: Felipe R. Monteiro felisous@amazon.com

• 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 #5893 (beb1353) into develop (45b6d72) will increase coverage by 0.07%.
The diff coverage is 97.66%.

@@             Coverage Diff             @@
##           develop    #5893      +/-   ##
===========================================
+ Coverage    72.95%   73.03%   +0.07%     
===========================================
  Files         1425     1429       +4     
  Lines       154281   154708     +427     
===========================================
+ Hits        112561   112990     +429     
+ Misses       41720    41718       -2     

Impacted Files	Coverage Δ
...ses/variable-sensitivity/constant_abstract_value.h	100.00% <ø> (ø)
...s/variable-sensitivity/value_set_abstract_object.h	100.00% <ø> (ø)
unit/analyses/variable-sensitivity/eval.cpp	100.00% <ø> (ø)
...lyses/variable-sensitivity/abstract_value_object.h	84.74% <83.63%> (-15.26%)	⬇️
src/linking/remove_internal_symbols.cpp	98.91% <91.66%> (-1.09%)	⬇️
...ses/variable-sensitivity/abstract_value_object.cpp	95.31% <95.88%> (+7.07%)	⬆️
...variable-sensitivity/value_set_abstract_object.cpp	86.99% <97.87%> (-4.73%)	⬇️
...-sensitivity/variable_sensitivity_test_helpers.cpp	98.23% <98.23%> (ø)
...lyses/variable-sensitivity/abstract_object_set.cpp	100.00% <100.00%> (ø)
...nalyses/variable-sensitivity/abstract_object_set.h	100.00% <100.00%> (ø)
... and 20 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 fa12ca7...beb1353. Read the comment docs.

[martin-cs]

This seems a reasonable and necessary step to get this working. I don't know the contract code as well as I should. Is there an option to ignore / disregard / drop the contracts? If so, does this add significant extra overhead? My feeling is probably not but I am not sure.

[feliperodri]

This seems a reasonable and necessary step to get this working. I don't know the contract code as well as I should. Is there an option to ignore / disregard / drop the contracts? If so, does this add significant extra overhead? My feeling is probably not but I am not sure.

Contracts are only added if you run goto-instrument with one of the following options:

Function contracts and invariants:
 --replace-call-with-contract <fun>
                              replace calls to fun with fun's contract
 --replace-all-calls-with-contracts
                              as above for all functions with a contract
 --enforce-contract <fun>     wrap fun with an assertion of its contract
 --enforce-all-contracts      as above for all functions with a contract

So you can choose which functions should use contracts or if they should be applied to all of them. I guess this confirms that there won't be any extra significant overhead. Did I answer your question, @martin-cs ?

[NlightNFotis]

LGTM.

[chrisr-diffblue]

LGTM, thanks.

[martin-cs]

@feliperodri yes and sorry for not getting back to you sooner. One minor concern -- what happens if there is recursion via the contracts?