CBMC
|
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 79 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 108 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 92 of file validate_types.cpp.