CBMC
|
The type of an expression, extends irept. More...
#include <type.h>
Public Member Functions | |
typet () | |
typet (const irep_idt &_id) | |
typet (irep_idt _id, typet _subtype) | |
typet & | add_subtype () |
bool | has_subtypes () const |
bool | has_subtype () const |
void | remove_subtype () |
const source_locationt & | source_location () const |
source_locationt & | add_source_location () |
typet & | add_type (const irep_idt &name) |
const typet & | find_type (const irep_idt &name) const |
![]() | |
bool | is_nil () const |
bool | is_not_nil () const |
irept (const irep_idt &_id) | |
irept (const irep_idt &_id, const named_subt &_named_sub, const subt &_sub) | |
irept ()=default | |
const irep_idt & | id () const |
const std::string & | id_string () const |
void | id (const irep_idt &_data) |
const irept & | find (const irep_idt &name) const |
irept & | add (const irep_idt &name) |
irept & | add (const irep_idt &name, irept irep) |
const std::string & | get_string (const irep_idt &name) const |
const irep_idt & | get (const irep_idt &name) const |
bool | get_bool (const irep_idt &name) const |
signed int | get_int (const irep_idt &name) const |
std::size_t | get_size_t (const irep_idt &name) const |
long long | get_long_long (const irep_idt &name) const |
void | set (const irep_idt &name, const irep_idt &value) |
void | set (const irep_idt &name, irept irep) |
void | set (const irep_idt &name, const long long value) |
void | set_size_t (const irep_idt &name, const std::size_t value) |
void | remove (const irep_idt &name) |
void | move_to_sub (irept &irep) |
void | move_to_named_sub (const irep_idt &name, irept &irep) |
bool | operator== (const irept &other) const |
bool | operator!= (const irept &other) const |
void | swap (irept &irep) |
bool | operator< (const irept &other) const |
defines ordering on the internal representation More... | |
bool | ordering (const irept &other) const |
defines ordering on the internal representation More... | |
int | compare (const irept &i) const |
defines ordering on the internal representation comments are ignored More... | |
void | clear () |
void | make_nil () |
subt & | get_sub () |
const subt & | get_sub () const |
named_subt & | get_named_sub () |
const named_subt & | get_named_sub () const |
std::size_t | hash () const |
std::size_t | full_hash () const |
bool | full_eq (const irept &other) const |
std::string | pretty (unsigned indent=0, unsigned max_indent=0) const |
![]() | |
sharing_treet (irep_idt _id) | |
sharing_treet (irep_idt _id, named_subt _named_sub, subt _sub) | |
sharing_treet () | |
sharing_treet (const sharing_treet &irep) | |
sharing_treet (sharing_treet &&irep) | |
sharing_treet & | operator= (const sharing_treet &irep) |
sharing_treet & | operator= (sharing_treet &&irep) |
~sharing_treet () | |
const dt & | read () const |
dt & | write () |
Static Public Member Functions | |
static void | check (const typet &, const validation_modet=validation_modet::INVARIANT) |
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked) More... | |
static void | validate (const typet &type, const namespacet &, const validation_modet vm=validation_modet::INVARIANT) |
Check that the type is well-formed, assuming that its subtypes have already been checked for well-formedness. More... | |
static void | validate_full (const typet &type, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT) |
Check that the type is well-formed (full check, including checks of subtypes) More... | |
![]() | |
static bool | is_comment (const irep_idt &name) |
static std::size_t | number_of_non_comments (const named_subt &) |
count the number of named_sub elements that are not comments More... | |
Additional Inherited Members | |
![]() | |
using | baset = tree_implementationt |
![]() | |
using | dt = tree_nodet< irept, forward_list_as_mapt< irep_idt, irept >, true > |
using | subt = typename dt::subt |
using | named_subt = typename dt::named_subt |
using | tree_implementationt = sharing_treet |
Used to refer to this class from derived classes. More... | |
![]() | |
void | detach () |
![]() | |
static void | remove_ref (dt *old_data) |
static void | nonrecursive_destructor (dt *old_data) |
Does the same as remove_ref, but using an explicit stack instead of recursion. More... | |
![]() | |
dt * | data |
![]() | |
static dt | empty_d |
The type of an expression, extends irept.
Types may have subtypes. This is modeled with two subs named “subtype” (a single type) and “subtypes” (a vector of types). The class typet only adds specialized methods for accessing the subtype information to the interface of irept. For pre-defined types see std_types.h
and mathematical_types.h
.
|
inline |
|
inlinestatic |
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)
Subclasses may override this function to provide specific well-formedness checks for the corresponding types.
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.
|
inline |
|
inlinestatic |
Check that the type is well-formed, assuming that its subtypes have already been checked for well-formedness.
Subclasses may override this function to provide specific well-formedness checks for the corresponding types.
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.
|
inlinestatic |
Check that the type is well-formed (full check, including checks of subtypes)
Subclasses may override this function, though in most cases the provided implementation should be sufficient.
The validation mode indicates whether well-formedness check failures are reported via DATA_INVARIANT violations or exceptions.