Go to the documentation of this file.
26 return val.find_first_not_of(
'0')==std::string::npos;
69 if(expr.
id()==ID_index)
84 else if(expr.
id()==ID_member)
98 else if(expr.
id()==ID_byte_extract_little_endian ||
99 expr.
id()==ID_byte_extract_big_endian)
112 else if(expr.
id()==ID_typecast)
120 else if(
const auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
123 if(
const auto address_of = expr_try_dynamic_cast<address_of_exprt>(pointer))
125 dest.
object() = address_of->object();
129 else if(
const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
132 if(
const auto deref = expr_try_dynamic_cast<dereference_exprt>(
object))
134 dest.
object() = deref->pointer();
148 if(
offset().
id()==ID_unknown)
158 const std::size_t _distance)
173 const std::size_t _upper,
174 const std::size_t _lower,
191 template <
typename T>
193 -> decltype(struct_expr.op0())
196 std::is_base_of<struct_exprt, T>::value,
"T must be a struct_exprt.");
200 index < struct_expr.operands().size(),
201 "component matching index should exist");
202 return struct_expr.operands()[index];
224 if(p->
id() == ID_member)
226 else if(p->
id() == ID_index)
251 const typet &compound_type = ns.
follow(member_expr.compound().type());
252 const auto *struct_union_type =
253 type_try_dynamic_cast<struct_union_typet>(compound_type);
256 struct_union_type !=
nullptr,
257 "member must address a struct, union or compatible type");
260 struct_union_type->get_component(member_expr.get_component_name());
265 "member component '" +
id2string(member_expr.get_component_name()) +
266 "' must exist on addressed type");
271 "member expression's type must match the addressed struct or union "
291 const typet &type_of_operand = dereference_expr.pointer().type();
294 type_try_dynamic_cast<pointer_typet>(type_of_operand);
299 "dereference expression's operand must have a pointer type");
304 "dereference expression's type must match the subtype of the type of its "
316 let_expr.values().size() == let_expr.variables().size(),
317 "number of variables must match number of values");
320 make_range(let_expr.variables()).zip(let_expr.values()))
325 "let binding symbols must be symbols");
330 "let bindings must be type consistent");
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
const typet & subtype() const
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Split an expression into a base object and a (byte) offset.
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
address_of_exprt(const exprt &op)
Unbounded, signed integers (mathematical integers, not bitvectors)
The plus expression Associativity is not specified.
Base class for all expressions.
Generic base class for unary expressions.
A base class for binary expressions.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
static void validate(const exprt &, validation_modet)
static void build_object_descriptor_rec(const namespacet &ns, const exprt &expr, object_descriptor_exprt &dest)
Build an object_descriptor_exprt from a given expr.
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
bitvector_typet index_type()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
unsigned int get_instance() const
Expression classes for byte-level operators.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::string & id2string(const irep_idt &d)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const exprt & compound() const
const exprt & struct_op() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
bool simplify(exprt &expr, const namespacet &ns)
Binary multiplication Associativity is not specified.
pointer_typet pointer_type(const typet &subtype)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
const irep_idt & id() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
std::vector< exprt > operandst
The Boolean constant false.
const exprt & root_object() const
Extract member of struct or union.
Deprecated expression utility functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
void set_instance(unsigned int instance)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool value_is_zero_string() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
exprt & component(const irep_idt &name, const namespacet &ns)
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The Boolean constant true.
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
API to expression classes.
binding_exprt & binding()
const irep_idt & get_value() const
ranget< iteratort > make_range(iteratort begin, iteratort end)
Base class for all expressions.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.