39 if(pointer.is_constant())
139 if(offset.has_value())
269 if(offset.has_value())
334 for(
const auto &op : ptr.
operands())
338 else if(!op.is_zero())
384 c_ptr.value_is_zero_string())
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
bitvector_typet c_index_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
struct configt::bv_encodingt bv_encoding
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
unsigned int get_instance() const
Base class for all expressions.
std::vector< exprt > operandst
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
The Boolean constant false.
The trinary if-then-else operator.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
irep_idt get_component_name() const
Binary multiplication Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
The plus expression Associativity is not specified.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
resultt simplify_inequality_address_of(const binary_relation_exprt &)
resultt simplify_good_pointer(const unary_exprt &)
static resultt changed(resultt<> result)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_pointer_offset(const unary_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_address_of_arg(const exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_object_size(const unary_exprt &)
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_plus(const plus_exprt &)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_node(exprt)
resultt simplify_pointer_object(const unary_exprt &)
const irep_idt & get_identifier() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
#define PRECONDITION(CONDITION)
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const string_constantt & to_string_constant(const exprt &expr)