CBMC
|
Go to the source code of this file.
Functions | |
void | check_expr (const exprt &expr, const validation_modet vm) |
Check that the given expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked) More... | |
void | validate_expr (const exprt &expr, const namespacet &ns, const validation_modet vm) |
Check that the given expression is well-formed, assuming that its subexpression and type have already been checked for well-formedness. More... | |
void | validate_full_expr (const exprt &expr, const namespacet &ns, const validation_modet vm) |
Check that the given expression is well-formed (full check, including checks of all subexpressions and the type) More... | |
void check_expr | ( | const exprt & | expr, |
const validation_modet | vm | ||
) |
Check that the given expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked)
The function determines the type T
of the expression expr
(by inspecting the id()
field) and then calls T::check(expr, vm)
.
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT
violations or exceptions.
Definition at line 85 of file validate_expressions.cpp.
void validate_expr | ( | const exprt & | expr, |
const namespacet & | ns, | ||
const validation_modet | vm | ||
) |
Check that the given expression is well-formed, assuming that its subexpression and type have already been checked for well-formedness.
The function determines the type T
of the expression expr
(by inspecting the id()
field) and then calls T::validate(expr, ns, vm)
.
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT
violations or exceptions.
Definition at line 98 of file validate_expressions.cpp.
void validate_full_expr | ( | const exprt & | expr, |
const namespacet & | ns, | ||
const validation_modet | vm | ||
) |
Check that the given expression is well-formed (full check, including checks of all subexpressions and the type)
The function determines the type T
of the expression expr
(by inspecting the id()
field) and then calls T::validate_full(expr, ns, vm)
.
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT
violations or exceptions.
Definition at line 114 of file validate_expressions.cpp.