CBMC
|
#include "validate_types.h"
#include "bitvector_types.h"
#include "c_types.h"
#include "validate_helpers.h"
Go to the source code of this file.
Macros | |
#define | CALL_ON_TYPE(type_type) C<typet, type_type>()(type, std::forward<Args>(args)...) |
Functions | |
template<template< typename, typename > class C, typename... Args> | |
void | call_on_type (const typet &type, Args &&... args) |
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... | |
#define CALL_ON_TYPE | ( | type_type | ) | C<typet, type_type>()(type, std::forward<Args>(args)...) |
Definition at line 19 of file validate_types.cpp.
void call_on_type | ( | const typet & | type, |
Args &&... | args | ||
) |
Definition at line 23 of file validate_types.cpp.
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.