add a 'language feature' facility for goto programs

[kroening]

This adds a facility to track the language features used by a goto program. The features are stored in the value of a symbol in the symbol table part of a goto model. The default, when not specificd, is true, i.e., we conservatively assume that the feature might be in use unless we know otherwise.

Checks for three language features not supported by goto symex are added (assembler, function pointers, vectors).

• 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.
• 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.

[remi-delmas-3000]

Hi Daniel,
would it be possible to also add a function that traverses the instructions of the GOTO functions and reports the presence/absence of the language features ? We could use this in DEBUG builds to check that the manually set flags match the goto model's contents. In release builds we just trust the tags.

[NlightNFotis]

Hello, we (@diffblue/diffblue-opensource) had a meeting to discuss the PR today, and while we're generally happy with the approach that is being taken, there are a few items that we would appreciate some clarity on:

1. This PR appears to be adding some of the language features, but seems to be missing others (say, language features transformed/eliminated by remove_returns, adjust_float_expressions, etc). Are there plans for these to be supported as part of this PR or perhaps a follow up PR?

2. This PR appears to be adding the infrastructure for setting language feature flags and seems to be unsetting those after the corresponding transformations have run, but we can't find where they are being set.

   We are assuming that these are going to be set in the various frontends (which will come around a bit later during this PR or in a follow up). Is our assumption correct?

3. We understand that one of the future aims for CBMC is to support analysis models that come from various different front-ends in the future.

   We believe that if CBMC is to work with multi-source-language models in the future, it will need to support knowledge of what language features are present on a per-function basis (because on a multi-source-language model, different front-ends might have applied different transformations to the models they produced, and thus, different functions might have different language features present).

   Is there some mechanism that would facilitate that, and if not, would it make sense to consider it early so that it doesn't pose significant challenges later?

4. One of the problems we were hoping to solve with our original proposed solution was the issue of multiple instrumentations being run on the same model, causing problems with multiple assertions being present in the model and reporting of results after analysis.

   This approach seems to be adding support for language features, but no mechanism to track instrumentations done. Would it be safe to assume that the same mechanism can be used to track instrumentations?

   If yes, would it make sense to keep the instrumentation symbols in the same list, or perhaps a different one?

   If not, what would be a proposed mechanism that would solve the multiple instrumentations issue.

[TGWDB]

Note that should/when #7736 is merged we should also assume that vectors cannot appear in symex-ready-goto.