Description
To check that the goto model is well-formed, we want to check that the symbol table and the goto functions are well-formed, and that the symbol table and the goto functions are consistent. This includes the well-formedness of instructions, statements, expressions, and types.
The overall framework is in PR #3123 (it might need to be adapted slightly as new checks are added). It descends into the goto model and calls the validate() methods on its various components. It also provides macros DATA_CHECK(condition, ...) which either throw an exception when the condition does not hold, or use DATA_INVARIANT() to check the condition (based on the validation mode).
PRs #3128, #3127, and #3118 check that the goto functions and the symbol table are consistent. Those checks will be integrated into the harness of #3123.
PRs checking that the goto functions are well formed, and that the symbol table is well-formed are upcoming.