Adds code contracts regression tests that involve function calls

[ArenBabikian]

This PR adds regression tests for code contracts.
7 test directories are added, for a total of 17 regression tests. They involves recursive and non-recursive function calls.

Among the 17 added tests, 7 are marked as KNOWNBUG, which means that they are skipped. Details for each test are specified in the corresponding test.desc file. The issues in these tests are solved by #5538.

---

• 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 #5911 (01444b7) into develop (99afbae) will increase coverage by 0.86%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #5911      +/-   ##
===========================================
+ Coverage    73.55%   74.41%   +0.86%     
===========================================
  Files         1431     1431              
  Lines       155245   159819    +4574     
===========================================
+ Hits        114188   118936    +4748     
+ Misses       41057    40883     -174     

Impacted Files	Coverage Δ
src/goto-symex/symex_main.cpp	81.79% <0.00%> (-4.18%)	⬇️
jbmc/src/java_bytecode/replace_java_nondet.cpp	91.33% <0.00%> (-2.53%)	⬇️
src/goto-programs/remove_vector.cpp	98.59% <0.00%> (-0.56%)	⬇️
jbmc/src/java_bytecode/remove_exceptions.cpp	95.48% <0.00%> (-0.09%)	⬇️
src/goto-instrument/rw_set.cpp	0.00% <0.00%> (ø)
src/goto-instrument/wmm/fence.cpp	0.00% <0.00%> (ø)
src/goto-programs/remove_skip.cpp	100.00% <0.00%> (ø)
unit/analyses/constant_propagator.cpp	100.00% <0.00%> (ø)
src/goto-instrument/wmm/goto2graph.cpp	0.00% <0.00%> (ø)
src/goto-instrument/wmm/shared_buffers.cpp	0.00% <0.00%> (ø)
... and 74 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 b2c7ab0...01444b7. Read the comment docs.

[feliperodri]

Didn't you find a way to update chan.sh to handle parameters for CBMC call as well?

[feliperodri]

LGTM.

[NlightNFotis]

LGTM.

Is there any plan to revisit the KNOWNBUG issues in the future and repair them?

[ArenBabikian]

LGTM.

Is there any plan to revisit the KNOWNBUG issues in the future and repair them?

Yes! once #5538 is merged, I will assess the KNOWNBUGs.