11#ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS
20#define CALL_ON_CODE(code_type) \
21 C<codet, code_type>()(code, std::forward<Args>(args)...)
20#define CALL_ON_CODE(code_type) \ …
23template <
template <
typename,
typename>
class C,
typename...
Args>
52#ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS
53 std::cerr <<
"Unimplemented well-formedness check for code statement with "
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
A goto_instruction_codet representing the removal of a local variable going out of scope.
A goto_instruction_codet representing the declaration of a local variable.
goto_instruction_codet representation of a function call statement.
goto_instruction_codet representation of a "return from a function" statement.
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void validate_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed, assuming that all its enclosed statements,...
void validate_full_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed (full check, including checks of all subexpression...
#define CALL_ON_CODE(code_type)
void check_code(const codet &code, const validation_modet vm)
Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements,...
void call_on_code(const codet &code, Args &&... args)