Go to the documentation of this file.
9 #ifndef CPROVER_UTIL_POINTER_EXPR_H
10 #define CPROVER_UTIL_POINTER_EXPR_H
51 return type.
id() == ID_pointer;
81 return type.
id() == ID_pointer && type.
subtype().
id() == ID_empty;
94 set(ID_C_reference,
true);
152 ID_object_descriptor,
161 ID_object_descriptor,
203 return base.
id() == ID_object_descriptor;
267 return base.
id() == ID_dynamic_object;
312 return base.
id() == ID_is_invalid_pointer;
325 expr.
operands().size() == 1,
"is_dynamic_object must have one operand");
335 expr.
operands().size() == 1,
"is_dynamic_object must have one operand");
346 :
unary_exprt(ID_address_of, std::move(
op), std::move(_type))
364 return base.
id() == ID_address_of;
403 return get(ID_identifier);
428 return base.
id() == ID_object_address;
505 return get(ID_component_name);
512 return expr.
id() == ID_field_address;
594 return expr.
id() == ID_element_address;
658 "dereference expression must have one operand");
670 return base.
id() == ID_dereference;
735 expr.
id() == ID_r_ok || expr.
id() == ID_w_ok || expr.
id() == ID_rw_ok);
777 #endif // CPROVER_UTIL_POINTER_EXPR_H
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
dynamic_object_exprt(typet type)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
const exprt & base() const
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
const typet & subtype() const
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
bool can_cast_expr< address_of_exprt >(const exprt &base)
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...
w_ok_exprt(exprt pointer, exprt size)
const exprt & index() const
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
The type of an expression, extends irept.
Operator to return the address of a field relative to a base address.
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
const typet & object_type() const
returns the type of the object whose address is represented
Operator to dereference a pointer.
Representation of heap-allocated objects.
Evaluates to true if the operand is a pointer to a dynamic object.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Split an expression into a base object and a (byte) offset.
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...
object_address_exprt(const symbol_exprt &)
field_address_exprt(exprt base, const irep_idt &component_name, pointer_typet type)
constructor for field addresses.
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
address_of_exprt(const exprt &op)
Base class for all expressions.
irep_idt object_identifier() const
Generic base class for unary expressions.
dereference_exprt(const exprt &op)
A base class for binary expressions.
const exprt & root_object() const
Expression to hold a symbol (variable)
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
const pointer_typet & type() const
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const exprt & pointer() const
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
symbol_exprt object_expr() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
An expression without operands.
bool get_bool(const irep_namet &name) const
unsigned int get_instance() const
Operator to return the address of an object.
const pointer_typet & type() const
address_of_exprt(exprt op, pointer_typet _type)
const exprt & pointer() const
const exprt & base() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
The null pointer constant.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
bool can_cast_expr< is_dynamic_object_exprt >(const exprt &base)
void validate_expr(const object_descriptor_exprt &value)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
pointer_typet(typet _subtype, std::size_t width)
const typet & field_type() const
returns the type of the field whose address is represented
dereference_exprt(exprt op, typet type)
Pre-defined bitvector types.
Fixed-width bit-vector with two's complement interpretation.
const typet & element_type() const
returns the type of the array element whose address is represented
bool can_cast_expr< dereference_exprt >(const exprt &base)
element_address_exprt(exprt base, exprt index)
constructor for element addresses.
null_pointer_exprt(pointer_typet type)
const exprt & valid() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
is_dynamic_object_exprt(const exprt &op)
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const irep_idt & id() const
const exprt & object() const
bool can_cast_expr< field_address_exprt >(const exprt &expr)
reference_typet(typet _subtype, std::size_t _width)
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
const irep_idt & component_name() const
r_ok_exprt(exprt pointer, exprt size)
object_descriptor_exprt(exprt _object)
const r_ok_exprt & to_r_ok_expr(const exprt &expr)
std::size_t get_width() const
reference_typet reference_type(const typet &subtype)
void set_instance(unsigned int instance)
bool can_cast_expr< element_address_exprt >(const exprt &expr)
bool is_reference(const typet &type)
Returns true if the type is a reference.
A predicate that indicates that an address range is ok to read.
const exprt & offset() const
Base class of fixed-width bit-vector types.
const irep_idt & get(const irep_namet &name) const
A predicate that indicates that an address range is ok to write.
void set(const irep_namet &name, const irep_idt &value)
const pointer_typet & type() const
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
A base class for a predicate that indicates that an address range is ok to read or write or both.
r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
bool can_cast_expr< object_address_exprt >(const exprt &base)
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
object_descriptor_exprt()
const exprt & object() const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & compound_type() const
A constant literal expression.
Operator to return the address of an array element relative to a base address.
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
API to expression classes.
const w_ok_exprt & to_w_ok_expr(const exprt &expr)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
signedbv_typet difference_type() const
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const exprt & size() const