9#ifndef CPROVER_UTIL_POINTER_EXPR_H
10#define CPROVER_UTIL_POINTER_EXPR_H
135 vm, type.
get_sub().size() == 1,
"reference must have one type parameter");
369 expr.
operands().size() == 1,
"is_dynamic_object must have one operand");
379 expr.
operands().size() == 1,
"is_dynamic_object must have one operand");
436 expr.
operands().size() == 3,
"pointer_in_range must have three operands");
446 expr.
operands().size() == 3,
"pointer_in_range must have three operands");
513 value, 5,
"prophecy_pointer_in_range must have five operands");
522 "prophecy_pointer_in_range must have five operands");
534 "prophecy_pointer_in_range must have five operands");
620 return type().base_type();
696 return type().base_type();
773 return type().base_type();
864 "dereference expression must have one operand");
1033 std::move(is_dead)})
1250 value, 1,
"Annotated pointer constant must have one operand");
1311 "pointer_offset must have pointer-typed operand");
1369 "pointer_object must have pointer-typed operand");
1451 "Object size expression must have pointer typed operand.");
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Pre-defined bitvector types.
reference_typet reference_type(const typet &subtype)
Operator to return the address of an object.
const exprt & object() const
address_of_exprt(exprt op, pointer_typet _type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
const irep_idt & get_value() const
void set_value(const irep_idt &value)
const exprt & symbolic_pointer() const
annotated_pointer_constant_exprt(const irep_idt &_value, const exprt &_pointer)
exprt & symbolic_pointer()
A base class for binary expressions.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Base class of fixed-width bit-vector types.
std::size_t get_width() const
std::size_t width() const
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
A constant literal expression.
An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that start...
cstrlen_exprt(exprt address, typet type)
const exprt & address() const
Operator to dereference a pointer.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
dereference_exprt(const exprt &op)
const exprt & pointer() const
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...
dereference_exprt(exprt op, typet type)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Representation of heap-allocated objects.
unsigned int get_instance() const
void set_instance(unsigned int instance)
const exprt & valid() const
dynamic_object_exprt(typet type)
Operator to return the address of an array element relative to a base address.
const typet & element_type() const
returns the type of the array element whose address is represented
const exprt & index() const
const pointer_typet & type() const
const exprt & base() const
Base class for all expressions.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
Operator to return the address of a field relative to a base address.
const typet & field_type() const
returns the type of the field whose address is represented
const exprt & base() const
const irep_idt & component_name() const
const typet & compound_type() const
const pointer_typet & type() const
bool get_bool(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
A predicate that indicates that a zero-terminated string starts at the given address.
const exprt & address() const
is_cstring_exprt(exprt address)
Evaluates to true if the operand is a pointer to a dynamic object.
is_dynamic_object_exprt(const exprt &op)
const exprt & address() const
A predicate that indicates that the object pointed to is live.
const exprt & pointer() const
live_object_exprt(exprt pointer)
A base class for multi-ary expressions Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
null_pointer_exprt(pointer_typet type)
An expression without operands.
Operator to return the address of an object.
const pointer_typet & type() const
symbol_exprt object_expr() const
irep_idt object_identifier() const
const typet & object_type() const
returns the type of the object whose address is represented
Split an expression into a base object and a (byte) offset.
object_descriptor_exprt()
const exprt & root_object() const
object_descriptor_exprt(exprt _object)
const exprt & offset() const
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 exprt & object() const
Expression for finding the size (in bytes) of the object a pointer points to.
object_size_exprt(exprt pointer, typet type)
const exprt & pointer() const
pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧...
pointer_in_range_exprt(exprt a, exprt b, exprt c)
const exprt & upper_bound() const
const exprt & lower_bound() const
const exprt & pointer() const
A numerical identifier for the object a pointer points to.
const exprt & pointer() const
pointer_object_exprt(exprt pointer, typet type)
The offset (in bytes) of a pointer relative to the object.
pointer_offset_exprt(exprt pointer, typet type)
const exprt & pointer() const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
signedbv_typet difference_type() const
const typet & base_type() const
The type of the data what we point to.
typet & base_type()
The type of the data what we point to.
pointer_typet(typet _base_type, std::size_t width)
const typet & subtype() const
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
const exprt & upper_bound() const
const exprt & dead_ptr() const
const exprt & lower_bound() const
const exprt & pointer() const
const exprt & deallocated_ptr() const
exprt lower(const namespacet &ns) const
prophecy_pointer_in_range_exprt(exprt a, exprt b, exprt c, exprt is_deallocated, exprt is_dead)
A predicate that indicates that an address range is ok to read.
prophecy_r_ok_exprt(exprt pointer, exprt size)
prophecy_r_ok_exprt(exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)
A base class for a predicate that indicates that an address range is ok to read or write or both.
prophecy_r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)
const exprt & deallocated_ptr() const
exprt lower(const namespacet &ns) const
Lower an r_or_w_ok_exprt to arithmetic and logic expressions.
const exprt & dead_ptr() const
const exprt & pointer() const
prophecy_r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
exprt & deallocated_ptr()
const exprt & size() const
A predicate that indicates that an address range is ok to write.
prophecy_w_ok_exprt(exprt pointer, exprt size)
prophecy_w_ok_exprt(exprt pointer, exprt size, exprt is_deallocated, exprt is_dead)
A predicate that indicates that an address range is ok to read.
r_ok_exprt(exprt pointer, exprt size)
A base class for a predicate that indicates that an address range is ok to read or write or both.
const exprt & size() const
r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
const exprt & pointer() const
reference_typet(typet _subtype, std::size_t _width)
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
A predicate that indicates that the objects pointed to are distinct.
separate_exprt(exprt::operandst __operands)
separate_exprt(exprt __op0, exprt __op1)
Fixed-width bit-vector with two's complement interpretation.
Expression to hold a symbol (variable)
An expression with three operands.
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
The type of an expression, extends irept.
Generic base class for unary expressions.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
A predicate that indicates that an address range is ok to write.
w_ok_exprt(exprt pointer, exprt size)
A predicate that indicates that the object pointed to is writeable.
writeable_object_exprt(exprt pointer)
const exprt & pointer() const
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
const live_object_exprt & to_live_object_expr(const exprt &expr)
Cast an exprt to a live_object_exprt.
bool can_cast_expr< separate_exprt >(const exprt &base)
const separate_exprt & to_separate_expr(const exprt &expr)
Cast an exprt to a separate_exprt.
void validate_expr(const object_descriptor_exprt &value)
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
const prophecy_r_ok_exprt & to_prophecy_r_ok_expr(const exprt &expr)
bool can_cast_expr< field_address_exprt >(const exprt &expr)
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const prophecy_w_ok_exprt & to_prophecy_w_ok_expr(const exprt &expr)
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
bool can_cast_expr< prophecy_w_ok_exprt >(const exprt &base)
bool can_cast_expr< live_object_exprt >(const exprt &base)
bool is_reference(const typet &type)
Returns true if the type is a reference.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)
Cast an exprt to an annotated_pointer_constant_exprt.
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const cstrlen_exprt & to_cstrlen_expr(const exprt &expr)
Cast an exprt to a cstrlen_exprt.
bool can_cast_expr< pointer_in_range_exprt >(const exprt &base)
bool can_cast_expr< prophecy_pointer_in_range_exprt >(const exprt &base)
bool can_cast_expr< dereference_exprt >(const exprt &base)
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
bool can_cast_expr< is_dynamic_object_exprt >(const exprt &base)
const writeable_object_exprt & to_writeable_object_expr(const exprt &expr)
Cast an exprt to a writeable_object_exprt.
bool can_cast_expr< cstrlen_exprt >(const exprt &base)
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
bool can_cast_expr< object_address_exprt >(const exprt &base)
const prophecy_pointer_in_range_exprt & to_prophecy_pointer_in_range_expr(const exprt &expr)
bool can_cast_expr< object_size_exprt >(const exprt &base)
bool can_cast_expr< is_cstring_exprt >(const exprt &base)
bool can_cast_expr< annotated_pointer_constant_exprt >(const exprt &base)
const pointer_in_range_exprt & to_pointer_in_range_expr(const exprt &expr)
bool can_cast_expr< address_of_exprt >(const exprt &base)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
bool can_cast_expr< pointer_offset_exprt >(const exprt &base)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
bool can_cast_expr< w_ok_exprt >(const exprt &base)
const w_ok_exprt & to_w_ok_expr(const exprt &expr)
const prophecy_r_or_w_ok_exprt & to_prophecy_r_or_w_ok_expr(const exprt &expr)
const r_ok_exprt & to_r_ok_expr(const exprt &expr)
bool can_cast_expr< element_address_exprt >(const exprt &expr)
bool can_cast_expr< r_ok_exprt >(const exprt &base)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
const is_cstring_exprt & to_is_cstring_expr(const exprt &expr)
Cast an exprt to a is_cstring_exprt.
bool can_cast_expr< r_or_w_ok_exprt >(const exprt &base)
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
const object_size_exprt & to_object_size_expr(const exprt &expr)
Cast an exprt to a object_size_exprt.
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
bool can_cast_expr< prophecy_r_or_w_ok_exprt >(const exprt &base)
bool can_cast_expr< writeable_object_exprt >(const exprt &base)
bool can_cast_expr< pointer_object_exprt >(const exprt &base)
bool can_cast_expr< prophecy_r_ok_exprt >(const exprt &base)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
API to expression classes.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...