|
CBMC
|
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Functions | |
| void | check_type (const typet &type, const validation_modet vm) |
| Check that the given type is well-formed (shallow checks only, i.e., subtypes are not checked) More... | |
| void | validate_type (const typet &type, const namespacet &ns, const validation_modet vm) |
| Check that the given type is well-formed, assuming that its subtypes have already been checked for well-formedness. More... | |
| void | validate_full_type (const typet &type, const namespacet &ns, const validation_modet vm) |
| Check that the given type is well-formed (full check, including checks of subtypes) More... | |
| void check_type | ( | const typet & | type, |
| const validation_modet | vm | ||
| ) |
Check that the given type is well-formed (shallow checks only, i.e., subtypes are not checked)
The function determines the type T of the type type (by inspecting the id() field) and then calls T::check(type, vm).
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.
Definition at line 80 of file validate_types.cpp.
| void validate_full_type | ( | const typet & | type, |
| const namespacet & | ns, | ||
| const validation_modet | vm | ||
| ) |
Check that the given type is well-formed (full check, including checks of subtypes)
The function determines the type T of the type type (by inspecting the id() field) and then calls T::validate_full(type, ns, vm).
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.
Definition at line 109 of file validate_types.cpp.
| void validate_type | ( | const typet & | type, |
| const namespacet & | ns, | ||
| const validation_modet | vm | ||
| ) |
Check that the given type is well-formed, assuming that its subtypes have already been checked for well-formedness.
The function determines the type T of the type type (by inspecting the id() field) and then calls T::validate(type, ns, vm).
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.
Definition at line 93 of file validate_types.cpp.