Go to the documentation of this file.
13 #ifndef CPROVER_UTIL_TYPE_H
14 #define CPROVER_UTIL_TYPE_H
35 #if defined(__clang__) || !defined(__GNUC__) || __GNUC__ >= 6
37 :
irept(std::move(_id), {}, {std::move(_subtype)})
43 subtype() = std::move(_subtype);
59 return static_cast<typet &
>(sub.front());
83 return static_cast<typet &
>(
add(name));
88 return static_cast<const typet &
>(
find(name));
149 :
typet(std::move(_id), std::move(_subtype))
158 {
return (
typet &)
add(ID_subtype); }
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)
231 #endif // CPROVER_UTIL_TYPE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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...
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)
type_with_subtypet(irep_idt _id, typet _subtype)
#define PRECONDITION(CONDITION)
const source_locationt & source_location() const
void move_to_subtypes(typet &type)
Move the provided type to the subtypes of this type.
void validate_type(const reference_typet &type)
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)
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
typet(irep_idt _id, typet _subtype)
typet remove_const(typet type)
Remove const qualifier from type (if any).
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irept & get_nil_irep()
typet & add_type(const irep_namet &name)
const typet & find_type(const irep_namet &name) const
typet(const irep_idt &_id)
type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes)