27 if(expr.
id()==ID_dereference &&
30 if(expr.
op0().
id()==ID_typecast &&
54 if(expr.
id()==ID_index)
92 else if(expr.
id()==ID_member)
102 if(op_type.
id()==ID_struct)
129 else if(expr.
id()==ID_dereference)
134 else if(expr.
id()==ID_if)
181 if(
object.
id()==ID_index)
196 else if(
object.
id()==ID_dereference)
199 assert(
object.operands().size()==1);
215 if(ptr.
id()==ID_if && ptr.
operands().size()==3)
226 if(ptr.
type().
id()!=ID_pointer)
229 if(ptr.
id()==ID_address_of)
242 else if(ptr.
id()==ID_typecast)
249 if(op_type.
id()==ID_pointer)
260 else if(op_type.
id()==ID_signedbv ||
261 op_type.
id()==ID_unsignedbv)
281 if(tmp.
id()==ID_plus && tmp.
operands().size()==2)
283 if(tmp.
op0().
id()==ID_typecast &&
285 tmp.
op0().
op0().
id()==ID_address_of)
288 if(type!=expr.
type())
294 else if(tmp.
op1().
id()==ID_typecast &&
296 tmp.
op1().
op0().
id()==ID_address_of)
299 if(type!=expr.
type())
309 else if(ptr.
id()==ID_plus)
314 for(
const auto &op : ptr.
operands())
316 if(op.type().id()==ID_pointer)
317 ptr_expr.push_back(op);
318 else if(!op.is_zero())
327 int_expr.push_back(tmp);
331 if(ptr_expr.size()!=1 || int_expr.empty())
334 typet pointer_sub_type=ptr_expr.front().type().
subtype();
335 if(pointer_sub_type.
id()==ID_empty)
350 if(int_expr.size()==1)
351 sum=int_expr.front();
373 else if(ptr.
id()==ID_constant)
398 number%=
power(2, offset_bits);
415 assert(expr.
type().
id()==ID_bool);
417 assert(expr.
id()==ID_equal || expr.
id()==ID_notequal);
420 if(tmp0.id()==ID_typecast)
422 if(tmp0.op0().id()==ID_index &&
426 if(tmp1.
id()==ID_typecast)
428 if(tmp1.
op0().
id()==ID_index &&
431 assert(tmp0.id()==ID_address_of);
432 assert(tmp1.
id()==ID_address_of);
434 if(tmp0.operands().size()!=1)
439 if(tmp0.op0().id()==ID_symbol &&
440 tmp1.
op0().
id()==ID_symbol)
455 assert(expr.
type().
id()==ID_bool);
457 assert(expr.
id()==ID_equal || expr.
id()==ID_notequal);
461 assert(it->id()==ID_pointer_object);
462 assert(it->operands().size()==1);
465 if(op.id()==ID_address_of)
467 if(op.operands().size()!=1 ||
468 (op.op0().id()!=ID_symbol &&
469 op.op0().id()!=ID_dynamic_object &&
470 op.op0().id()!=ID_string_constant))
473 else if(op.id()!=ID_constant ||
474 op.get(ID_value)!=ID_NULL)
499 exprt p_o_false=expr;
537 if(op.
id()==ID_constant && op.
get(ID_value)==ID_NULL)
544 if(op.
id()==ID_address_of && op.
operands().size()==1)
546 if(op.
op0().
id()==ID_symbol)
554 else if(op.
op0().
id()==ID_string_constant)
559 else if(op.
op0().
id()==ID_array)
582 if(op.
id()==ID_constant && op.
get(ID_value)==ID_NULL)
589 if(op.
id()==ID_address_of)
603 if(a.
id()==ID_address_of && b.
id()==ID_address_of &&
607 if(a.
id()==ID_constant && b.
id()==ID_constant &&
608 a.
get(ID_value)==ID_NULL && b.
get(ID_value)==ID_NULL)
611 if(a.
id()==ID_constant && b.
id()==ID_address_of &&
612 a.
get(ID_value)==ID_NULL)
615 if(b.
id()==ID_constant && a.
id()==ID_address_of &&
616 b.
get(ID_value)==ID_NULL)
627 if(a.
id()==ID_symbol && b.
id()==ID_symbol)
632 else if(a.
id()==ID_index && b.
id()==ID_index)
637 else if(a.
id()==ID_member && b.
id()==ID_member)
658 if(op.
id()==ID_address_of && op.
operands().size()==1)
660 if(op.
op0().
id()==ID_symbol)
671 if(size.
type()!=type)
681 else if(op.
op0().
id()==ID_string_constant)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
bool simplify_pointer_object(exprt &expr)
bool simplify_node(exprt &expr)
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
Deprecated expression utility functions.
bool simplify_dynamic_object(exprt &expr)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
const irep_idt & get_identifier() const
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
const irep_idt & get_value() const
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
bool simplify_inequality_pointer_object(exprt &expr)
The trinary if-then-else operator.
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
bool simplify_address_of_arg(exprt &expr)
A constant literal expression.
void make_bool(bool value)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
bool value_is_zero_string() const
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
struct configt::bv_encodingt bv_encoding
bool simplify_if(if_exprt &expr)
const irep_idt & id() const
bool simplify_good_pointer(exprt &expr)
bool simplify_object(exprt &expr)
A generic base class for binary expressions.
Operator to dereference a pointer.
bool simplify_address_of(exprt &expr)
API to expression classes.
bool simplify_pointer_offset(exprt &expr)
const irep_idt & get(const irep_namet &name) const
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Operator to return the address of an object.
Various predicates over pointers in programs.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
The boolean constant false.
std::vector< exprt > operandst
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
static tvt objects_equal(const exprt &a, const exprt &b)
bool simplify_rec(exprt &expr)
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Base class for all expressions.
exprt pointer_offset(const exprt &pointer)
irep_idt get_component_name() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
bool simplify_inequality_address_of(exprt &expr)
const typet & subtype() const
bool simplify_invalid_pointer(exprt &expr)
bool simplify_object_size(exprt &expr)
void make_typecast(const typet &_type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
bitvector_typet char_type()