CBMC
validate_expressions.h File Reference
+ This graph shows which files directly or indirectly include this file:

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

Function Documentation

◆ check_expr()

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.

◆ validate_expr()

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.

◆ validate_full_expr()

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.