31 "nil array size must be exactly nil");
51 const irep_idt &component_name)
const
57 if(c.get_name() == component_name)
68 const irep_idt &component_name)
const
72 if(c.get_name() == component_name)
98 :
exprt(ID_base, std::move(base))
109 for(
const auto &b :
bases())
126 if(ot_components.size()<
127 tt_components.size())
130 componentst::const_iterator
131 ot_it=ot_components.begin();
133 for(
const auto &tt_c : tt_components)
135 if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name())
149 return type.
id()==ID_pointer &&
156 return type.
id()==ID_pointer &&
157 type.
get_bool(ID_C_rvalue_reference);
220 const auto has_constant_components = [&ns](
const typet &
subtype) ->
bool {
224 for(
const auto &
component : struct_union_type.components())
248 if(type.
id() == ID_pointer)
249 return type.
get_bool(ID_C_constant);
256 if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
258 const auto &resolved_type = ns.
follow(type);
259 return has_constant_components(resolved_type);
301 for(
const auto &comp : comps)
305 if(!element_width.has_value())
308 if(max_width.has_value() && *element_width <= *max_width)
311 max_width = *element_width;
312 max_comp_type = comp.type();
313 max_comp_name = comp.get_name();
316 if(!max_width.has_value())
319 return std::make_pair(
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
const exprt & size() const
mp_integer min_value() const
mp_integer max_value() 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.
std::size_t get_integer_bits() const
std::size_t get_f() const
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
mp_integer largest() const
Return the largest value that can be represented using this type.
constant_exprt zero_expr() const
Return an expression representing the zero value of this type.
constant_exprt smallest_expr() const
Return an expression representing the smallest value of this type.
mp_integer smallest() const
Return the smallest value that can be represented using this type.
irept & add(const irep_namet &name)
void set(const irep_namet &name, const irep_idt &value)
const std::string & get_string(const irep_namet &name) const
bool get_bool(const irep_namet &name) const
tree_implementationt baset
const irept & find(const irep_namet &name) const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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)
void set_from(const mp_integer &_from)
mp_integer get_to() const
mp_integer get_from() const
A struct tag type, i.e., struct_typet with an identifier.
struct_tag_typet & type()
Structure type, corresponds to C style structs.
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 basest & bases() const
Get the collection of base classes/structs.
optionalt< baset > get_base(const irep_idt &id) const
Return the base with the given name, if exists.
const typet & component_type(const irep_idt &component_name) const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
const componentst & components() const
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
const irep_idt & get_identifier() const
Type with a single subtype.
The type of an expression, extends irept.
const typet & subtype() const
optionalt< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
vector_typet(const typet &_subtype, const constant_exprt &_size)
const constant_exprt & size() const
const irept & get_nil_irep()
const std::string & id2string(const irep_idt &d)
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
nonstd::optional< T > optionalt
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#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.
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.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
unsigned unsafe_string2unsigned(const std::string &str, int base)
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,...