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 const irept & get_nil_irep()
The type of an expression, extends irept.
bool has_subtypes() const
typet(const irep_idt &_id)
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 type_with_subtypest & to_type_with_subtypes(const typet &type)
std::vector< irept > subt
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)
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)
Type with multiple subtypes.
type_with_subtypet(const irep_idt &_id, const typet &_subtype)
typet(const irep_idt &_id, const typet &_subtype)
const type_with_subtypet & to_type_with_subtype(const typet &type)
static void check(const typet &, const validation_modet)
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)
const subtypest & subtypes() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
Base class for tree-like data structures with sharing.
Type with a single subtype.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void validate_type(const typet &)
Called after casting.
void move_to_subtypes(typet &type)
Move the provided type to the subtypes of this type.
const source_locationt & source_location() const
type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
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 typet & find_type(const irep_namet &name) const
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...
source_locationt & add_source_location()
void copy_to_subtypes(const typet &type)
Copy the provided type to the subtypes of this type.
irept & add(const irep_namet &name)
typet & add_type(const irep_namet &name)
std::vector< typet > subtypest
const typet & subtype() const
const irept & find(const irep_namet &name) const