enable --validate-goto-model for all cbmc regressions

[kroening]

This will prevent the introduction of changes that violate the checks
in the goto-validation procedure.

This will need more work to actually pass CI; at the moment, basically all tests fail.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a 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).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[tautschnig]

This is tempting, but I think it's wrong: we do not have proper dependency tracking here (tests should be re-run whenever either the binary or the tests themselves change).

[kroening]

Ok, I'll simply make "test" the default target.

[chrisr-diffblue]

Sounds great if we can turn this on. One issue we've discovered recently is with the symbol checks that form part of --validate-goto-model failing on the return symbol, e.g. the following example:

int main(){
    return 0;
}

currently fails if passed through --validate-goto-model:

cbmc return.c --validate-goto-model
CBMC version 5.9 (cbmc-5.9-381-g32d7a6b89) 64-bit x86_64 macos
Parsing return.c
Converting
Type-checking return
Generating GOTO Program
Symbol is malformed:  (at: )

<< EXTRA DIAGNOSTICS >>
return'
<< END EXTRA DIAGNOSTICS >>

which I suspect is accounting for a large number of the CI failures when this option is enabled....

[chrisr-diffblue]

This particular symbol.is_well_formed() check was added in #3193

[chrisr-diffblue]

So #3193 added a test that : has_suffix(id2string(name), id2string(base_name))) - and this seems to not be the case for a number of cases, such as the return' symbol created for the entry point function, compound symbols created by c_typecheck_baset::typecheck_compound_type and possibly other cases.

[kroening]

@chrisr-diffblue I can well imagine a few more cases where we might use suffixes on the identifier to disambiguate; say we are doing that for C++ and Java method overloading.

[chrisr-diffblue]

@kroening So can we enumerate what makes a symbol 'well formed' ? We can remove this suffix check if that's not something that we expect to hold, which would leave 'well formed' simply being "has a mode".

[allredj]

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 745351e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96270244
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

[chrisr-diffblue]

@kroening - I'm working at the moment on getting the symbol wellformedness checks working so that you won't have to revert df616e4 - I'll let you know when I have something that is useable.

[tautschnig]

This has been merged as part of #3767.