30 "nil array size must be exactly nil");
48 const irep_idt &component_name)
const
54 if(
c.get_name() == component_name)
65 const irep_idt &component_name)
const
69 if(
c.get_name() == component_name)
104std::optional<struct_typet::baset>
107 for(
const auto &
b :
bases())
128 componentst::const_iterator
170 return get_from() <= singleton && singleton <= get_to();
288 size() = std::move(_size);
bitvector_typet c_index_type()
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
typet index_type() const
The type of the index expressions into any instance of this type.
std::size_t width() const
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
bool get_bool(const irep_idt &name) const
std::size_t get_size_t(const irep_idt &name) const
const irept & find(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
irept & add(const irep_idt &name)
const std::string & get_string(const irep_idt &name) const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void set_to(const mp_integer &to)
constant_exprt zero_expr() const
void set_from(const mp_integer &_from)
mp_integer get_to() const
bool includes(const mp_integer &) const
constant_exprt one_expr() const
mp_integer get_from() const
A struct tag type, i.e., struct_typet with an identifier.
Base class or struct that a class or struct inherits from.
baset(struct_tag_typet base)
struct_tag_typet & type()
Structure type, corresponds to C style structs.
const basest & bases() const
Get the collection of base classes/structs.
std::optional< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
bool is_prefix_of(const struct_typet &other) const
Returns true if the struct is a prefix of other, i.e., if this struct has n components then the compo...
void add_base(const struct_tag_typet &base)
Add a base class/struct.
const typet & component_type(const irep_idt &component_name) const
const componentst & components() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
std::vector< componentt > componentst
Type with a single subtype.
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
The type of an expression, extends irept.
vector_typet(typet index_type, typet element_type, constant_exprt size)
const constant_exprt & size() const
typet & index_type_nonconst()
The type of any index expression into an instance of this type.
typet index_type() const
The type of any index expression into an instance of this type.
const irept & get_nil_irep()
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
bool is_reference(const typet &type)
Returns true if the type is a reference.
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify whether a given type is constant itself or contains constant components.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const type_with_subtypet & to_type_with_subtype(const typet &type)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...