Go to the documentation of this file.
27 if(expr.
id()==ID_dereference &&
30 if(expr.
op0().
id()==ID_typecast &&
54 if(expr.
id()==ID_index)
73 if(step_size.has_value())
96 else if(expr.
id()==ID_member)
106 if(op_type.
id()==ID_struct)
117 if(offset.has_value())
133 else if(expr.
id()==ID_dereference)
138 else if(expr.
id()==ID_if)
185 if(
object.
id()==ID_index)
200 else if(
object.
id()==ID_dereference)
204 expr = object_as_dereference_expr.pointer();
218 if(ptr.
id()==ID_if && ptr.
operands().size()==3)
229 if(ptr.
type().
id()!=ID_pointer)
232 if(ptr.
id()==ID_address_of)
239 if(offset.has_value())
245 else if(ptr.
id()==ID_typecast)
252 if(op_type.
id()==ID_pointer)
263 else if(op_type.
id()==ID_signedbv ||
264 op_type.
id()==ID_unsignedbv)
284 if(tmp.
id()==ID_plus && tmp.
operands().size()==2)
286 if(tmp.
op0().
id()==ID_typecast &&
288 tmp.
op0().
op0().
id()==ID_address_of)
291 if(type!=expr.
type())
297 else if(tmp.
op1().
id()==ID_typecast &&
299 tmp.
op1().
op0().
id()==ID_address_of)
302 if(type!=expr.
type())
312 else if(ptr.
id()==ID_plus)
317 for(
const auto &op : ptr.
operands())
319 if(op.type().id()==ID_pointer)
320 ptr_expr.push_back(op);
321 else if(!op.is_zero())
330 int_expr.push_back(tmp);
334 if(ptr_expr.size()!=1 || int_expr.empty())
337 typet pointer_sub_type=ptr_expr.front().type().
subtype();
338 if(pointer_sub_type.
id()==ID_empty)
343 if(!element_size.has_value())
352 if(int_expr.size()==1)
353 sum=int_expr.front();
374 else if(ptr.
id()==ID_constant)
400 number%=
power(2, offset_bits);
418 expr.
operands().size() == 2,
"(in)equalities have two operands");
421 if(tmp0.id()==ID_typecast)
423 if(tmp0.op0().id()==ID_index &&
427 if(tmp1.
id()==ID_typecast)
429 if(tmp1.
op0().
id()==ID_index &&
432 INVARIANT(tmp0.id() == ID_address_of,
"id must be ID_address_of");
433 INVARIANT(tmp1.
id() == ID_address_of,
"id must be ID_address_of");
435 if(tmp0.operands().size()!=1)
440 if(tmp0.op0().id()==ID_symbol &&
441 tmp1.
op0().
id()==ID_symbol)
459 expr.
operands().size() == 2,
"(in)equalities have two operands");
467 if(op.id()==ID_address_of)
469 if(op.operands().size()!=1 ||
470 (op.op0().id()!=ID_symbol &&
471 op.op0().id()!=ID_dynamic_object &&
472 op.op0().id()!=ID_string_constant))
475 else if(op.id()!=ID_constant ||
476 op.get(ID_value)!=ID_NULL)
501 exprt p_o_false=expr;
539 if(op.
id()==ID_constant && op.
get(ID_value)==ID_NULL)
546 if(op.
id()==ID_address_of && op.
operands().size()==1)
548 if(op.
op0().
id()==ID_symbol)
556 else if(op.
op0().
id()==ID_string_constant)
561 else if(op.
op0().
id()==ID_array)
584 if(op.
id()==ID_constant && op.
get(ID_value)==ID_NULL)
591 if(op.
id()==ID_address_of)
605 if(a.
id()==ID_address_of && b.
id()==ID_address_of &&
609 if(a.
id()==ID_constant && b.
id()==ID_constant &&
610 a.
get(ID_value)==ID_NULL && b.
get(ID_value)==ID_NULL)
613 if(a.
id()==ID_constant && b.
id()==ID_address_of &&
614 a.
get(ID_value)==ID_NULL)
617 if(b.
id()==ID_constant && a.
id()==ID_address_of &&
618 b.
get(ID_value)==ID_NULL)
629 if(a.
id()==ID_symbol && b.
id()==ID_symbol)
634 else if(a.
id()==ID_index && b.
id()==ID_index)
639 else if(a.
id()==ID_member && b.
id()==ID_member)
660 if(op.
id()==ID_address_of && op.
operands().size()==1)
662 if(op.
op0().
id()==ID_symbol)
673 if(size.
type() != expr_type)
683 else if(op.
op0().
id()==ID_string_constant)
bool simplify_node(exprt &expr)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
bool simplify_pointer_object(exprt &expr)
const typet & subtype() const
bool simplify_inequality_pointer_object(exprt &expr)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
The type of an expression, extends irept.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Operator to dereference a pointer.
The trinary if-then-else operator.
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
The plus expression Associativity is not specified.
Base class for all expressions.
A base class for binary expressions.
struct configt::ansi_ct ansi_c
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
bool is_true() const
Return whether the expression is a constant representing true.
bitvector_typet index_type()
bool simplify_dynamic_object(exprt &expr)
bool is_false() const
Return whether the expression is a constant representing false.
bool simplify_good_pointer(exprt &expr)
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
struct configt::bv_encodingt bv_encoding
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
typet & type()
Return the type of the expression.
bool simplify_inequality_address_of(exprt &expr)
exprt size_of_expr(const typet &type, const namespacet &ns)
const std::string & id2string(const irep_idt &d)
#define forall_operands(it, expr)
const irep_idt & get_identifier() const
bool simplify_invalid_pointer(exprt &expr)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
bool simplify_object_size(exprt &expr)
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
std::vector< exprt > operandst
The Boolean constant false.
bool simplify_pointer_offset(exprt &expr)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt pointer_offset(const exprt &pointer)
bitvector_typet char_type()
bool is_zero() const
Return whether the expression is a constant representing 0.
Deprecated expression utility functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
static tvt objects_equal(const exprt &a, const exprt &b)
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
Structure type, corresponds to C style structs.
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
bool value_is_zero_string() const
bool simplify_address_of(exprt &expr)
bool simplify_rec(exprt &expr)
bool is_constant() const
Return whether the expression is a constant.
bool simplify_object(exprt &expr)
bool simplify_if(if_exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
bool has_prefix(const std::string &s, const std::string &prefix)
irep_idt get_component_name() const
Operator to return the address of an object.
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
bool simplify_address_of_arg(exprt &expr)
A constant literal expression.
const irep_idt & get_value() const
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.