Go to the documentation of this file.
13 #ifndef CPROVER_UTIL_TYPE_H
14 #define CPROVER_UTIL_TYPE_H
42 return static_cast<const typet &>(
get_sub().front());
50 return static_cast<typet &>(sub.front());
69 return static_cast<source_locationt &>(
add(ID_C_source_location));
74 return static_cast<typet &>(
add(name));
79 return static_cast<const typet &>(
find(name));
138 DEPRECATED(
"use type_with_subtypet(id, subtype) instead")
152 {
return (
typet &)
add(ID_subtype); }
159 return static_cast<const type_with_subtypet &>(type);
165 return static_cast<type_with_subtypet &>(type);
174 DEPRECATED(
"use type_with_subtypest(id, subtypes) instead")
177 DEPRECATED(
"use type_with_subtypest(id, subtypes) instead")
208 return static_cast<const type_with_subtypest &>(type);
213 return static_cast<type_with_subtypest &>(type);
216 #define forall_subtypes(it, type) \
217 if((type).has_subtypes()) \
218 for(type_with_subtypest::subtypest::const_iterator it=to_type_with_subtypes(type).subtypes().begin(), \
219 it##_end=to_type_with_subtypes(type).subtypes().end(); \
222 #define Forall_subtypes(it, type) \
223 if((type).has_subtypes()) \
224 for(type_with_subtypest::subtypest::iterator it=to_type_with_subtypes(type).subtypes().begin(); \
225 it!=to_type_with_subtypes(type).subtypes().end(); ++it)
227 #endif // CPROVER_UTIL_TYPE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
void copy_to_subtypes(const typet &type)
Copy the provided type to the subtypes of this type.
const typet & subtype() const
Type with multiple subtypes.
std::vector< typet > subtypest
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 type of an expression, extends irept.
irept & add(const irep_namet &name)
bool has_subtypes() const
const irept & find(const irep_namet &name) const
const type_with_subtypet & to_type_with_subtype(const typet &type)
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Type with a single subtype.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void validate_type(const typet &)
Called after casting.
type_with_subtypet(const irep_idt &_id, const typet &_subtype)
typet(const irep_idt &_id, const typet &_subtype)
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
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)
const source_locationt & source_location() const
static void check(const typet &, const validation_modet)
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)
void move_to_subtypes(typet &type)
Move the provided type to the subtypes of this type.
source_locationt & add_source_location()
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-for...
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)
const subtypest & subtypes() const
Base class for tree-like data structures with sharing.
const irept & get_nil_irep()
typet & add_type(const irep_namet &name)
const typet & find_type(const irep_namet &name) const
std::vector< irept > subt
typet(const irep_idt &_id)
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)