Go to the documentation of this file.
27 (expr.
id() == ID_symbol &&
47 if(expr.
id()==ID_index)
51 else if(expr.
id()==ID_member)
99 if(subtype.
id() == ID_empty)
101 if(object_expr.
id() == ID_string_constant)
103 subtype = object_expr.
type();
109 if(array_size > pointer.
offset)
115 auto deep_object_opt =
118 exprt deep_object = deep_object_opt.value();
static exprt conditional_cast(const exprt &expr, const typet &type)
void get_dynamic_objects(std::vector< std::size_t > &objects) const
const typet & subtype() const
#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.
Various predicates over pointers in programs.
std::size_t add_object(const exprt &expr)
The plus expression Associativity is not specified.
Base class for all expressions.
pointer_logict(const namespacet &_ns)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
irep_idt byte_extract_id()
typet & type()
Return the type of the expression.
hash_numbering< exprt, irep_hash > objects
bool get_bool(const irep_namet &name) const
Expression classes for byte-level operators.
The null pointer constant.
const std::string & id2string(const irep_idt &d)
#define SYMEX_DYNAMIC_PREFIX
bool simplify(exprt &expr, const namespacet &ns)
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
exprt object_size(const exprt &pointer)
const irep_idt & id() const
bitvector_typet char_type()
bool is_zero() const
Return whether the expression is a constant representing 0.
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.
bool is_dynamic_object(const exprt &expr) const
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::size_t invalid_object
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
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)
Operator to return the address of an object.
Semantic type conversion.
signedbv_typet pointer_diff_type()
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A constant literal expression.
API to expression classes.
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.