Add CBMC primitive regression tests to new SMT2 backend

[esteffin]

Add all supported and working CBMC primitive regression tests to the new SMT2 backend.

At the moment the following CBMC primitives regressions are not supported or working.

A report on that will be adde shortly

• 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 #7044 (15f2d13) into develop (8258529) will decrease coverage by 0.02%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #7044      +/-   ##
===========================================
- Coverage    77.88%   77.86%   -0.03%     
===========================================
  Files         1569     1569              
  Lines       180995   180995              
===========================================
- Hits        140968   140929      -39     
- Misses       40027    40066      +39     

Impacted Files	Coverage Δ
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp	82.18% <0.00%> (-6.38%)	⬇️

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

[tautschnig]

Please try to keep the corresponding Makefile in sync with this change.

[NlightNFotis]

This PR is affected by the issue described in #7054, hence the cancelled CI run for check-ubuntu-20_04-cmake-gcc-THOROUGH.

Despite this, I believe this PR shouldn't be held up by that, as the files changed here don't affect the issue at all.

[NlightNFotis]

A report on that will be adde shortly

Is the report going to be attached to this PR? Or is this going somewhere else? @esteffin

[esteffin]

State of the regression tests:

Not working

Unimplemented SMT generation for expression: address_of

• regression/cbmc-primitives/alternating_quantifiers_6231/exists_in_forall.desc
• regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.desc
• regression/cbmc-primitives/dynamic-object-01/test.desc
• regression/cbmc-primitives/exists_assume_6231/test2.desc
• regression/cbmc-primitives/implication_statement_checks_1/test.desc
• regression/cbmc-primitives/object-size-01/test.desc
• regression/cbmc-primitives/object-size-01/test-no-cp.desc

Unimplemented SMT generation for expression: is_dynamic_object

• regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc
• regression/cbmc-primitives/dynamic-object-02/test.desc

Unimplemented SMT generation for expression: tuple

• regression/cbmc-primitives/exists_assume_6231/test.desc

Unimplemented SMT generation for expression: nondet_symbol

• regression/cbmc-primitives/dynamic-object-01/test-no-cp.desc
• regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc
• regression/cbmc-primitives/exists_memory_checks/negated_exists.desc
• regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc
• regression/cbmc-primitives/r_w_ok_inconsistent_dead/test-no-cp.desc
• regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/test.desc
• regression/cbmc-primitives/r_w_ok_inconsistent_deallocated/test-no-cp.desc
• regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test-no-cp.desc
• regression/cbmc-primitives/r_w_ok_inconsistent_nondet/test.desc
• regression/cbmc-primitives/r_w_ok_valid/test-no-cp.desc
• regression/cbmc-primitives/r_w_ok_valid_negated/test-no-cp.desc
• regression/cbmc-primitives/same-object-01/test-no-cp.desc
• regression/cbmc-primitives/same-object-02/test-no-cp.desc
• regression/cbmc-primitives/same-object-03/test-no-cp.desc
• regression/cbmc-primitives/same-object-04/test-no-cp.desc

Specifically uses the old backend -z3:

• regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

Unimplemented SMT generation for expression: convert_expr_to_smt::minus_exprt doesn't handle expressions whereonly one operand is a pointer: [1]

• regression/cbmc-primitives/r_w_ok_bug/test.desc

Error: couldn't find function with name 'test_global_pointer' in symbol table

• regression/cbmc-primitives/r_w_ok_inconsistent_dead/test.desc

Result is wrong. Expected 2 FAILURE, got SUCCESS and FAILURE.

• regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc
• regression/cbmc-primitives/pointer-offset-01/test.desc

Ignored

Marked FUTURE:

• regression/cbmc-primitives/r_w_ok_inconsistent_integer/test-no-cp.desc
• regression/cbmc-primitives/r_w_ok_inconsistent_integer/test.desc

Working:

• regression/cbmc-primitives/forall_6231_1/test.desc
• regression/cbmc-primitives/forall_6231_2/test.desc
• regression/cbmc-primitives/forall_6231_3/test.desc
• regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc
• regression/cbmc-primitives/forall_6231_4/test.desc
• regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc
• regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc
• regression/cbmc-primitives/r_w_ok_null/test-no-cp.desc
• regression/cbmc-primitives/r_w_ok_null/test.desc
• regression/cbmc-primitives/r_w_ok_valid/test.desc
• regression/cbmc-primitives/r_w_ok_valid_negated/test.desc
• regression/cbmc-primitives/same-object-01/test.desc
• regression/cbmc-primitives/same-object-02/test.desc
• regression/cbmc-primitives/same-object-03/test.desc
• regression/cbmc-primitives/same-object-04/test.desc

[1] Reason: Reached unimplemented convert_expr_to_smt::minus_exprt doesn't handle expressions whereonly one operand is a pointer - this is because these expressionsare normally handled by convert_expr_to_smt::plus_exprt due totransformations of the expressions by previous passes bringingthem into a form more suitably handled by that version of the function.If you are here, this is a mistake or something went wrong before.The expression that caused the problem is: