API to expression classes for Pointers. More...

#include "bitvector_types.h"
#include "std_expr.h"

Include dependency graph for pointer_expr.h:

Classes
class	pointer_typet
	The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype). More...
class	reference_typet
	The reference type. More...
class	object_descriptor_exprt
	Split an expression into a base object and a (byte) offset. More...
class	dynamic_object_exprt
	Representation of heap-allocated objects. More...
class	is_dynamic_object_exprt
	Evaluates to true if the operand is a pointer to a dynamic object. More...
class	pointer_in_range_exprt
	pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧ a<=b ∧ b<=c Note that the last inequality is weak, i.e., b may be equal to c. More...
class	prophecy_pointer_in_range_exprt
	pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer refers to a deallocated or out-of-scope object. More...
class	address_of_exprt
	Operator to return the address of an object. More...
class	object_address_exprt
	Operator to return the address of an object. More...
class	field_address_exprt
	Operator to return the address of a field relative to a base address. More...
class	element_address_exprt
	Operator to return the address of an array element relative to a base address. More...
class	dereference_exprt
	Operator to dereference a pointer. More...
class	null_pointer_exprt
	The null pointer constant. More...
class	r_or_w_ok_exprt
	A base class for a predicate that indicates that an address range is ok to read or write or both. More...
class	r_ok_exprt
	A predicate that indicates that an address range is ok to read. More...
class	w_ok_exprt
	A predicate that indicates that an address range is ok to write. More...
class	prophecy_r_or_w_ok_exprt
	A base class for a predicate that indicates that an address range is ok to read or write or both. More...
class	prophecy_r_ok_exprt
	A predicate that indicates that an address range is ok to read. More...
class	prophecy_w_ok_exprt
	A predicate that indicates that an address range is ok to write. More...
class	annotated_pointer_constant_exprt
	Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the numeric representation of. More...
class	pointer_offset_exprt
	The offset (in bytes) of a pointer relative to the object. More...
class	pointer_object_exprt
	A numerical identifier for the object a pointer points to. More...
class	object_size_exprt
	Expression for finding the size (in bytes) of the object a pointer points to. More...
class	is_cstring_exprt
	A predicate that indicates that a zero-terminated string starts at the given address. More...
class	cstrlen_exprt
	An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that starts at the given address. More...
class	live_object_exprt
	A predicate that indicates that the object pointed to is live. More...
class	writeable_object_exprt
	A predicate that indicates that the object pointed to is writeable. More...
class	separate_exprt
	A predicate that indicates that the objects pointed to are distinct. More...

Functions
template<>
bool	can_cast_type< pointer_typet > (const typet &type)
	Check whether a reference to a typet is a pointer_typet.
const pointer_typet &	to_pointer_type (const typet &type)
	Cast a typet to a pointer_typet.
pointer_typet &	to_pointer_type (typet &type)
	Cast a typet to a pointer_typet.
bool	is_void_pointer (const typet &type)
	This method tests, if the given typet is a pointer of type void.
template<>
bool	can_cast_type< reference_typet > (const typet &type)
	Check whether a reference to a typet is a reference_typet.
const reference_typet &	to_reference_type (const typet &type)
	Cast a typet to a reference_typet.
reference_typet &	to_reference_type (typet &type)
	Cast a typet to a reference_typet.
bool	is_reference (const typet &type)
	Returns true if the type is a reference.
bool	is_rvalue_reference (const typet &type)
	Returns if the type is an R value reference.
template<>
bool	can_cast_expr< object_descriptor_exprt > (const exprt &base)
void	validate_expr (const object_descriptor_exprt &value)
const object_descriptor_exprt &	to_object_descriptor_expr (const exprt &expr)
	Cast an exprt to an object_descriptor_exprt.
object_descriptor_exprt &	to_object_descriptor_expr (exprt &expr)
	Cast an exprt to an object_descriptor_exprt.
template<>
bool	can_cast_expr< dynamic_object_exprt > (const exprt &base)
void	validate_expr (const dynamic_object_exprt &value)
const dynamic_object_exprt &	to_dynamic_object_expr (const exprt &expr)
	Cast an exprt to a dynamic_object_exprt.
dynamic_object_exprt &	to_dynamic_object_expr (exprt &expr)
	Cast an exprt to a dynamic_object_exprt.
template<>
bool	can_cast_expr< is_dynamic_object_exprt > (const exprt &base)
void	validate_expr (const is_dynamic_object_exprt &value)
const is_dynamic_object_exprt &	to_is_dynamic_object_expr (const exprt &expr)
is_dynamic_object_exprt &	to_is_dynamic_object_expr (exprt &expr)
template<>
bool	can_cast_expr< pointer_in_range_exprt > (const exprt &base)
void	validate_expr (const pointer_in_range_exprt &value)
const pointer_in_range_exprt &	to_pointer_in_range_expr (const exprt &expr)
pointer_in_range_exprt &	to_pointer_in_range_expr (exprt &expr)
template<>
bool	can_cast_expr< prophecy_pointer_in_range_exprt > (const exprt &base)
void	validate_expr (const prophecy_pointer_in_range_exprt &value)
const prophecy_pointer_in_range_exprt &	to_prophecy_pointer_in_range_expr (const exprt &expr)
prophecy_pointer_in_range_exprt &	to_prophecy_pointer_in_range_expr (exprt &expr)
template<>
bool	can_cast_expr< address_of_exprt > (const exprt &base)
void	validate_expr (const address_of_exprt &value)
const address_of_exprt &	to_address_of_expr (const exprt &expr)
	Cast an exprt to an address_of_exprt.
address_of_exprt &	to_address_of_expr (exprt &expr)
	Cast an exprt to an address_of_exprt.
template<>
bool	can_cast_expr< object_address_exprt > (const exprt &base)
void	validate_expr (const object_address_exprt &value)
const object_address_exprt &	to_object_address_expr (const exprt &expr)
	Cast an exprt to an object_address_exprt.
object_address_exprt &	to_object_address_expr (exprt &expr)
	Cast an exprt to an object_address_exprt.
template<>
bool	can_cast_expr< field_address_exprt > (const exprt &expr)
void	validate_expr (const field_address_exprt &value)
const field_address_exprt &	to_field_address_expr (const exprt &expr)
	Cast an exprt to an field_address_exprt.
field_address_exprt &	to_field_address_expr (exprt &expr)
	Cast an exprt to an field_address_exprt.
template<>
bool	can_cast_expr< element_address_exprt > (const exprt &expr)
void	validate_expr (const element_address_exprt &value)
const element_address_exprt &	to_element_address_expr (const exprt &expr)
	Cast an exprt to an element_address_exprt.
element_address_exprt &	to_element_address_expr (exprt &expr)
	Cast an exprt to an element_address_exprt.
template<>
bool	can_cast_expr< dereference_exprt > (const exprt &base)
void	validate_expr (const dereference_exprt &value)
const dereference_exprt &	to_dereference_expr (const exprt &expr)
	Cast an exprt to a dereference_exprt.
dereference_exprt &	to_dereference_expr (exprt &expr)
	Cast an exprt to a dereference_exprt.
template<>
bool	can_cast_expr< r_or_w_ok_exprt > (const exprt &base)
void	validate_expr (const r_or_w_ok_exprt &value)
const r_or_w_ok_exprt &	to_r_or_w_ok_expr (const exprt &expr)
template<>
bool	can_cast_expr< r_ok_exprt > (const exprt &base)
void	validate_expr (const r_ok_exprt &value)
const r_ok_exprt &	to_r_ok_expr (const exprt &expr)
template<>
bool	can_cast_expr< w_ok_exprt > (const exprt &base)
void	validate_expr (const w_ok_exprt &value)
const w_ok_exprt &	to_w_ok_expr (const exprt &expr)
template<>
bool	can_cast_expr< prophecy_r_or_w_ok_exprt > (const exprt &base)
void	validate_expr (const prophecy_r_or_w_ok_exprt &value)
const prophecy_r_or_w_ok_exprt &	to_prophecy_r_or_w_ok_expr (const exprt &expr)
template<>
bool	can_cast_expr< prophecy_r_ok_exprt > (const exprt &base)
void	validate_expr (const prophecy_r_ok_exprt &value)
const prophecy_r_ok_exprt &	to_prophecy_r_ok_expr (const exprt &expr)
template<>
bool	can_cast_expr< prophecy_w_ok_exprt > (const exprt &base)
void	validate_expr (const prophecy_w_ok_exprt &value)
const prophecy_w_ok_exprt &	to_prophecy_w_ok_expr (const exprt &expr)
template<>
bool	can_cast_expr< annotated_pointer_constant_exprt > (const exprt &base)
void	validate_expr (const annotated_pointer_constant_exprt &value)
const annotated_pointer_constant_exprt &	to_annotated_pointer_constant_expr (const exprt &expr)
	Cast an exprt to an annotated_pointer_constant_exprt.
annotated_pointer_constant_exprt &	to_annotated_pointer_constant_expr (exprt &expr)
	Cast an exprt to an annotated_pointer_constant_exprt.
template<>
bool	can_cast_expr< pointer_offset_exprt > (const exprt &base)
void	validate_expr (const pointer_offset_exprt &value)
const pointer_offset_exprt &	to_pointer_offset_expr (const exprt &expr)
	Cast an exprt to a pointer_offset_exprt.
pointer_offset_exprt &	to_pointer_offset_expr (exprt &expr)
	Cast an exprt to a pointer_offset_exprt.
template<>
bool	can_cast_expr< pointer_object_exprt > (const exprt &base)
void	validate_expr (const pointer_object_exprt &value)
const pointer_object_exprt &	to_pointer_object_expr (const exprt &expr)
	Cast an exprt to a pointer_object_exprt.
pointer_object_exprt &	to_pointer_object_expr (exprt &expr)
	Cast an exprt to a pointer_object_exprt.
const object_size_exprt &	to_object_size_expr (const exprt &expr)
	Cast an exprt to a object_size_exprt.
object_size_exprt &	to_object_size_expr (exprt &expr)
	Cast an exprt to a object_size_exprt.
template<>
bool	can_cast_expr< object_size_exprt > (const exprt &base)
void	validate_expr (const object_size_exprt &value)
template<>
bool	can_cast_expr< is_cstring_exprt > (const exprt &base)
void	validate_expr (const is_cstring_exprt &value)
const is_cstring_exprt &	to_is_cstring_expr (const exprt &expr)
	Cast an exprt to a is_cstring_exprt.
is_cstring_exprt &	to_is_cstring_expr (exprt &expr)
	Cast an exprt to a is_cstring_exprt.
template<>
bool	can_cast_expr< cstrlen_exprt > (const exprt &base)
void	validate_expr (const cstrlen_exprt &value)
const cstrlen_exprt &	to_cstrlen_expr (const exprt &expr)
	Cast an exprt to a cstrlen_exprt.
cstrlen_exprt &	to_cstrlen_expr (exprt &expr)
	Cast an exprt to a cstrlen_exprt.
template<>
bool	can_cast_expr< live_object_exprt > (const exprt &base)
void	validate_expr (const live_object_exprt &value)
const live_object_exprt &	to_live_object_expr (const exprt &expr)
	Cast an exprt to a live_object_exprt.
live_object_exprt &	to_live_object_expr (exprt &expr)
	Cast an exprt to a live_object_exprt.
template<>
bool	can_cast_expr< writeable_object_exprt > (const exprt &base)
void	validate_expr (const writeable_object_exprt &value)
const writeable_object_exprt &	to_writeable_object_expr (const exprt &expr)
	Cast an exprt to a writeable_object_exprt.
writeable_object_exprt &	to_writeable_object_expr (exprt &expr)
	Cast an exprt to a writeable_object_exprt.
template<>
bool	can_cast_expr< separate_exprt > (const exprt &base)
void	validate_expr (const separate_exprt &value)
const separate_exprt &	to_separate_expr (const exprt &expr)
	Cast an exprt to a separate_exprt.
separate_exprt &	to_separate_expr (exprt &expr)
	Cast an exprt to a separate_exprt.

Detailed Description

API to expression classes for Pointers.

Definition in file pointer_expr.h.

Function Documentation

◆ can_cast_expr< address_of_exprt >()

template<>

bool can_cast_expr< address_of_exprt > ( const exprt & base )

inline

Definition at line 558 of file pointer_expr.h.

◆ can_cast_expr< annotated_pointer_constant_exprt >()

template<>

bool can_cast_expr< annotated_pointer_constant_exprt > ( const exprt & base )

inline

Definition at line 1239 of file pointer_expr.h.

◆ can_cast_expr< cstrlen_exprt >()

template<>

bool can_cast_expr< cstrlen_exprt > ( const exprt & base )

inline

Definition at line 1533 of file pointer_expr.h.

◆ can_cast_expr< dereference_exprt >()

template<>

bool can_cast_expr< dereference_exprt > ( const exprt & base )

inline

Definition at line 871 of file pointer_expr.h.

◆ can_cast_expr< dynamic_object_exprt >()

template<>

bool can_cast_expr< dynamic_object_exprt > ( const exprt & base )

inline

Definition at line 299 of file pointer_expr.h.

◆ can_cast_expr< element_address_exprt >()

template<>

bool can_cast_expr< element_address_exprt > ( const exprt & expr )

inline

Definition at line 795 of file pointer_expr.h.

◆ can_cast_expr< field_address_exprt >()

template<>

bool can_cast_expr< field_address_exprt > ( const exprt & expr )

inline

Definition at line 708 of file pointer_expr.h.

◆ can_cast_expr< is_cstring_exprt >()

template<>

bool can_cast_expr< is_cstring_exprt > ( const exprt & base )

inline

Definition at line 1475 of file pointer_expr.h.

◆ can_cast_expr< is_dynamic_object_exprt >()

template<>

bool can_cast_expr< is_dynamic_object_exprt > ( const exprt & base )

inline

Definition at line 354 of file pointer_expr.h.

◆ can_cast_expr< live_object_exprt >()

template<>

bool can_cast_expr< live_object_exprt > ( const exprt & base )

inline

Definition at line 1589 of file pointer_expr.h.

◆ can_cast_expr< object_address_exprt >()

template<>

bool can_cast_expr< object_address_exprt > ( const exprt & base )

inline

Definition at line 624 of file pointer_expr.h.

◆ can_cast_expr< object_descriptor_exprt >()

template<>

bool can_cast_expr< object_descriptor_exprt > ( const exprt & base )

inline

Definition at line 235 of file pointer_expr.h.

◆ can_cast_expr< object_size_exprt >()

template<>

bool can_cast_expr< object_size_exprt > ( const exprt & base )

inline

Definition at line 1438 of file pointer_expr.h.

◆ can_cast_expr< pointer_in_range_exprt >()

template<>

bool can_cast_expr< pointer_in_range_exprt > ( const exprt & base )

inline

Definition at line 421 of file pointer_expr.h.

◆ can_cast_expr< pointer_object_exprt >()

template<>

bool can_cast_expr< pointer_object_exprt > ( const exprt & base )

inline

Definition at line 1356 of file pointer_expr.h.

◆ can_cast_expr< pointer_offset_exprt >()

template<>

bool can_cast_expr< pointer_offset_exprt > ( const exprt & base )

inline

Definition at line 1298 of file pointer_expr.h.

◆ can_cast_expr< prophecy_pointer_in_range_exprt >()

template<>

bool can_cast_expr< prophecy_pointer_in_range_exprt > ( const exprt & base )

inline

Definition at line 503 of file pointer_expr.h.

◆ can_cast_expr< prophecy_r_ok_exprt >()

template<>

bool can_cast_expr< prophecy_r_ok_exprt > ( const exprt & base )

inline

Definition at line 1131 of file pointer_expr.h.

◆ can_cast_expr< prophecy_r_or_w_ok_exprt >()

template<>

bool can_cast_expr< prophecy_r_or_w_ok_exprt > ( const exprt & base )

inline

Definition at line 1080 of file pointer_expr.h.

◆ can_cast_expr< prophecy_w_ok_exprt >()

template<>

bool can_cast_expr< prophecy_w_ok_exprt > ( const exprt & base )

inline

Definition at line 1179 of file pointer_expr.h.

◆ can_cast_expr< r_ok_exprt >()

template<>

bool can_cast_expr< r_ok_exprt > ( const exprt & base )

inline

Definition at line 966 of file pointer_expr.h.

◆ can_cast_expr< r_or_w_ok_exprt >()

template<>

bool can_cast_expr< r_or_w_ok_exprt > ( const exprt & base )

inline

Definition at line 936 of file pointer_expr.h.

◆ can_cast_expr< separate_exprt >()

template<>

bool can_cast_expr< separate_exprt > ( const exprt & base )

inline

Definition at line 1699 of file pointer_expr.h.

◆ can_cast_expr< w_ok_exprt >()

template<>

bool can_cast_expr< w_ok_exprt > ( const exprt & base )

inline

Definition at line 995 of file pointer_expr.h.

◆ can_cast_expr< writeable_object_exprt >()

template<>

bool can_cast_expr< writeable_object_exprt > ( const exprt & base )

inline

Definition at line 1645 of file pointer_expr.h.

◆ can_cast_type< pointer_typet >()

template<>

bool can_cast_type< pointer_typet > ( const typet & type )

inline

Check whether a reference to a typet is a pointer_typet.

Parameters

type	Source type.

Returns: True if type is a pointer_typet.

Definition at line 80 of file pointer_expr.h.

◆ can_cast_type< reference_typet >()

template<>

bool can_cast_type< reference_typet > ( const typet & type )

inline

Check whether a reference to a typet is a reference_typet.

Parameters

type	Source type.

Returns: True if type is a reference_typet.

Definition at line 149 of file pointer_expr.h.

◆ is_reference()

bool is_reference ( const typet & type )

Returns true if the type is a reference.

Definition at line 145 of file std_types.cpp.

◆ is_rvalue_reference()

bool is_rvalue_reference ( const typet & type )

Returns if the type is an R value reference.

Definition at line 152 of file std_types.cpp.

◆ is_void_pointer()

bool is_void_pointer ( const typet & type )

inline

This method tests, if the given typet is a pointer of type void.

Definition at line 110 of file pointer_expr.h.

◆ to_address_of_expr() [1/2]

const address_of_exprt & to_address_of_expr ( const exprt & expr )

inline

Cast an exprt to an address_of_exprt.

expr must be known to be address_of_exprt.

Parameters

expr	Source expression

Returns: Object of type address_of_exprt

Definition at line 574 of file pointer_expr.h.

◆ to_address_of_expr() [2/2]

address_of_exprt & to_address_of_expr ( exprt & expr )

inline

Cast an exprt to an address_of_exprt.

expr must be known to be address_of_exprt.

Parameters

expr	Source expression

Returns: Object of type address_of_exprt

Definition at line 583 of file pointer_expr.h.

◆ to_annotated_pointer_constant_expr() [1/2]

const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr ( const exprt & expr )

inline

Cast an exprt to an annotated_pointer_constant_exprt.

expr must be known to be annotated_pointer_constant_exprt.

Parameters

expr	Source expression

Returns: Object of type annotated_pointer_constant_exprt

Definition at line 1257 of file pointer_expr.h.

◆ to_annotated_pointer_constant_expr() [2/2]

annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr ( exprt & expr )

inline

Cast an exprt to an annotated_pointer_constant_exprt.

expr must be known to be annotated_pointer_constant_exprt.

Parameters

expr	Source expression

Returns: Object of type annotated_pointer_constant_exprt

Definition at line 1268 of file pointer_expr.h.

◆ to_cstrlen_expr() [1/2]

const cstrlen_exprt & to_cstrlen_expr ( const exprt & expr )

inline

Cast an exprt to a cstrlen_exprt.

expr must be known to be cstrlen_exprt.

Parameters

expr	Source expression

Returns: Object of type cstrlen_exprt

Definition at line 1549 of file pointer_expr.h.

◆ to_cstrlen_expr() [2/2]

cstrlen_exprt & to_cstrlen_expr ( exprt & expr )

inline

Cast an exprt to a cstrlen_exprt.

expr must be known to be cstrlen_exprt.

Parameters

expr	Source expression

Returns: Object of type cstrlen_exprt

Definition at line 1558 of file pointer_expr.h.

◆ to_dereference_expr() [1/2]

const dereference_exprt & to_dereference_expr ( const exprt & expr )

inline

Cast an exprt to a dereference_exprt.

expr must be known to be dereference_exprt.

Parameters

expr	Source expression

Returns: Object of type dereference_exprt

Definition at line 887 of file pointer_expr.h.

◆ to_dereference_expr() [2/2]

dereference_exprt & to_dereference_expr ( exprt & expr )

inline

Cast an exprt to a dereference_exprt.

expr must be known to be dereference_exprt.

Parameters

expr	Source expression

Returns: Object of type dereference_exprt

Definition at line 896 of file pointer_expr.h.

◆ to_dynamic_object_expr() [1/2]

const dynamic_object_exprt & to_dynamic_object_expr ( const exprt & expr )

inline

Cast an exprt to a dynamic_object_exprt.

expr must be known to be dynamic_object_exprt.

Parameters

expr	Source expression

Returns: Object of type dynamic_object_exprt

Definition at line 315 of file pointer_expr.h.

◆ to_dynamic_object_expr() [2/2]

dynamic_object_exprt & to_dynamic_object_expr ( exprt & expr )

inline

Cast an exprt to a dynamic_object_exprt.

expr must be known to be dynamic_object_exprt.

Parameters

expr	Source expression

Returns: Object of type dynamic_object_exprt

Definition at line 325 of file pointer_expr.h.

◆ to_element_address_expr() [1/2]

const element_address_exprt & to_element_address_expr ( const exprt & expr )

inline

Cast an exprt to an element_address_exprt.

expr must be known to be element_address_exprt.

Parameters

expr	Source expression

Returns: Object of type element_address_exprt

Definition at line 811 of file pointer_expr.h.

◆ to_element_address_expr() [2/2]

element_address_exprt & to_element_address_expr ( exprt & expr )

inline

Cast an exprt to an element_address_exprt.

expr must be known to be element_address_exprt.

Parameters

expr	Source expression

Returns: Object of type element_address_exprt

Definition at line 821 of file pointer_expr.h.

◆ to_field_address_expr() [1/2]

const field_address_exprt & to_field_address_expr ( const exprt & expr )

inline

Cast an exprt to an field_address_exprt.

expr must be known to be field_address_exprt.

Parameters

expr	Source expression

Returns: Object of type field_address_exprt

Definition at line 724 of file pointer_expr.h.

◆ to_field_address_expr() [2/2]

field_address_exprt & to_field_address_expr ( exprt & expr )

inline

Cast an exprt to an field_address_exprt.

expr must be known to be field_address_exprt.

Parameters

expr	Source expression

Returns: Object of type field_address_exprt

Definition at line 734 of file pointer_expr.h.

◆ to_is_cstring_expr() [1/2]

const is_cstring_exprt & to_is_cstring_expr ( const exprt & expr )

inline

Cast an exprt to a is_cstring_exprt.

expr must be known to be is_cstring_exprt.

Parameters

expr	Source expression

Returns: Object of type is_cstring_exprt

Definition at line 1491 of file pointer_expr.h.

◆ to_is_cstring_expr() [2/2]

is_cstring_exprt & to_is_cstring_expr ( exprt & expr )

inline

Cast an exprt to a is_cstring_exprt.

expr must be known to be is_cstring_exprt.

Parameters

expr	Source expression

Returns: Object of type is_cstring_exprt

Definition at line 1500 of file pointer_expr.h.

◆ to_is_dynamic_object_expr() [1/2]

const is_dynamic_object_exprt & to_is_dynamic_object_expr ( const exprt & expr )

inline

Definition at line 365 of file pointer_expr.h.

◆ to_is_dynamic_object_expr() [2/2]

is_dynamic_object_exprt & to_is_dynamic_object_expr ( exprt & expr )

inline

Definition at line 374 of file pointer_expr.h.

◆ to_live_object_expr() [1/2]

const live_object_exprt & to_live_object_expr ( const exprt & expr )

inline

Cast an exprt to a live_object_exprt.

expr must be known to be live_object_exprt.

Parameters

expr	Source expression

Returns: Object of type live_object_exprt

Definition at line 1605 of file pointer_expr.h.

◆ to_live_object_expr() [2/2]

live_object_exprt & to_live_object_expr ( exprt & expr )

inline

Cast an exprt to a live_object_exprt.

expr must be known to be live_object_exprt.

Parameters

expr	Source expression

Returns: Object of type live_object_exprt

Definition at line 1614 of file pointer_expr.h.

◆ to_object_address_expr() [1/2]

const object_address_exprt & to_object_address_expr ( const exprt & expr )

inline

Cast an exprt to an object_address_exprt.

expr must be known to be object_address_exprt.

Parameters

expr	Source expression

Returns: Object of type object_address_exprt

Definition at line 640 of file pointer_expr.h.

◆ to_object_address_expr() [2/2]

object_address_exprt & to_object_address_expr ( exprt & expr )

inline

Cast an exprt to an object_address_exprt.

expr must be known to be object_address_exprt.

Parameters

expr	Source expression

Returns: Object of type object_address_exprt

Definition at line 650 of file pointer_expr.h.

◆ to_object_descriptor_expr() [1/2]

const object_descriptor_exprt & to_object_descriptor_expr ( const exprt & expr )

inline

Cast an exprt to an object_descriptor_exprt.

expr must be known to be object_descriptor_exprt.

Parameters

expr	Source expression

Returns: Object of type object_descriptor_exprt

Definition at line 252 of file pointer_expr.h.

◆ to_object_descriptor_expr() [2/2]

object_descriptor_exprt & to_object_descriptor_expr ( exprt & expr )

inline

Cast an exprt to an object_descriptor_exprt.

expr must be known to be object_descriptor_exprt.

Parameters

expr	Source expression

Returns: Object of type object_descriptor_exprt

Definition at line 262 of file pointer_expr.h.

◆ to_object_size_expr() [1/2]

const object_size_exprt & to_object_size_expr ( const exprt & expr )

inline

Cast an exprt to a object_size_exprt.

expr must be known to be object_size_exprt.

Parameters

expr	Source expression

Returns: Object of type object_size_exprt

Definition at line 1420 of file pointer_expr.h.

◆ to_object_size_expr() [2/2]

object_size_exprt & to_object_size_expr ( exprt & expr )

inline

Cast an exprt to a object_size_exprt.

expr must be known to be object_size_exprt.

Parameters

expr	Source expression

Returns: Object of type object_size_exprt

Definition at line 1429 of file pointer_expr.h.

◆ to_pointer_in_range_expr() [1/2]

const pointer_in_range_exprt & to_pointer_in_range_expr ( const exprt & expr )

inline

Definition at line 431 of file pointer_expr.h.

◆ to_pointer_in_range_expr() [2/2]

pointer_in_range_exprt & to_pointer_in_range_expr ( exprt & expr )

inline

Definition at line 440 of file pointer_expr.h.

◆ to_pointer_object_expr() [1/2]

const pointer_object_exprt & to_pointer_object_expr ( const exprt & expr )

inline

Cast an exprt to a pointer_object_exprt.

expr must be known to be pointer_object_exprt.

Parameters

expr	Source expression

Returns: Object of type pointer_object_exprt

Definition at line 1375 of file pointer_expr.h.

◆ to_pointer_object_expr() [2/2]

pointer_object_exprt & to_pointer_object_expr ( exprt & expr )

inline

Cast an exprt to a pointer_object_exprt.

expr must be known to be pointer_object_exprt.

Parameters

expr	Source expression

Returns: Object of type pointer_object_exprt

Definition at line 1385 of file pointer_expr.h.

◆ to_pointer_offset_expr() [1/2]

const pointer_offset_exprt & to_pointer_offset_expr ( const exprt & expr )

inline

Cast an exprt to a pointer_offset_exprt.

expr must be known to be pointer_offset_exprt.

Parameters

expr	Source expression

Returns: Object of type pointer_offset_exprt

Definition at line 1317 of file pointer_expr.h.

◆ to_pointer_offset_expr() [2/2]

pointer_offset_exprt & to_pointer_offset_expr ( exprt & expr )

inline

Cast an exprt to a pointer_offset_exprt.

expr must be known to be pointer_offset_exprt.

Parameters

expr	Source expression

Returns: Object of type pointer_offset_exprt

Definition at line 1327 of file pointer_expr.h.

◆ to_pointer_type() [1/2]

const pointer_typet & to_pointer_type ( const typet & type )

inline

Cast a typet to a pointer_typet.

This is an unchecked conversion. type must be known to be pointer_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type pointer_typet.

Definition at line 93 of file pointer_expr.h.

◆ to_pointer_type() [2/2]

pointer_typet & to_pointer_type ( typet & type )

inline

Cast a typet to a pointer_typet.

This is an unchecked conversion. type must be known to be pointer_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type pointer_typet.

Definition at line 101 of file pointer_expr.h.

◆ to_prophecy_pointer_in_range_expr() [1/2]

const prophecy_pointer_in_range_exprt & to_prophecy_pointer_in_range_expr ( const exprt & expr )

inline

Definition at line 515 of file pointer_expr.h.

◆ to_prophecy_pointer_in_range_expr() [2/2]

prophecy_pointer_in_range_exprt & to_prophecy_pointer_in_range_expr ( exprt & expr )

inline

Definition at line 526 of file pointer_expr.h.

◆ to_prophecy_r_ok_expr()

const prophecy_r_ok_exprt & to_prophecy_r_ok_expr ( const exprt & expr )

inline

Definition at line 1141 of file pointer_expr.h.

◆ to_prophecy_r_or_w_ok_expr()

const prophecy_r_or_w_ok_exprt & to_prophecy_r_or_w_ok_expr ( const exprt & expr )

inline

Definition at line 1092 of file pointer_expr.h.

◆ to_prophecy_w_ok_expr()

const prophecy_w_ok_exprt & to_prophecy_w_ok_expr ( const exprt & expr )

inline

Definition at line 1189 of file pointer_expr.h.

◆ to_r_ok_expr()

const r_ok_exprt & to_r_ok_expr ( const exprt & expr )

inline

Definition at line 976 of file pointer_expr.h.

◆ to_r_or_w_ok_expr()

const r_or_w_ok_exprt & to_r_or_w_ok_expr ( const exprt & expr )

inline

Definition at line 946 of file pointer_expr.h.

◆ to_reference_type() [1/2]

const reference_typet & to_reference_type ( const typet & type )

inline

Cast a typet to a reference_typet.

This is an unchecked conversion. type must be known to be reference_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type reference_typet.

Definition at line 162 of file pointer_expr.h.

◆ to_reference_type() [2/2]

reference_typet & to_reference_type ( typet & type )

inline

Cast a typet to a reference_typet.

This is an unchecked conversion. type must be known to be reference_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns: Object of type reference_typet.

Definition at line 169 of file pointer_expr.h.

◆ to_separate_expr() [1/2]

const separate_exprt & to_separate_expr ( const exprt & expr )

inline

Cast an exprt to a separate_exprt.

expr must be known to be separate_exprt.

Parameters

expr	Source expression

Returns: Object of type separate_exprt

Definition at line 1714 of file pointer_expr.h.

◆ to_separate_expr() [2/2]

separate_exprt & to_separate_expr ( exprt & expr )

inline

Cast an exprt to a separate_exprt.

expr must be known to be separate_exprt.

Parameters

expr	Source expression

Returns: Object of type separate_exprt

Definition at line 1723 of file pointer_expr.h.

◆ to_w_ok_expr()

const w_ok_exprt & to_w_ok_expr ( const exprt & expr )

inline

Definition at line 1005 of file pointer_expr.h.

◆ to_writeable_object_expr() [1/2]

const writeable_object_exprt & to_writeable_object_expr ( const exprt & expr )

inline

Cast an exprt to a writeable_object_exprt.

expr must be known to be writeable_object_exprt.

Parameters

expr	Source expression

Returns: Object of type writeable_object_exprt

Definition at line 1661 of file pointer_expr.h.

◆ to_writeable_object_expr() [2/2]

writeable_object_exprt & to_writeable_object_expr ( exprt & expr )

inline

Cast an exprt to a writeable_object_exprt.

expr must be known to be writeable_object_exprt.

Parameters

expr	Source expression

Returns: Object of type writeable_object_exprt

Definition at line 1671 of file pointer_expr.h.

◆ validate_expr() [1/25]

void validate_expr ( const address_of_exprt & value )

inline

Definition at line 563 of file pointer_expr.h.

◆ validate_expr() [2/25]

void validate_expr ( const annotated_pointer_constant_exprt & value )

inline

Definition at line 1244 of file pointer_expr.h.

◆ validate_expr() [3/25]

void validate_expr ( const cstrlen_exprt & value )

inline

Definition at line 1538 of file pointer_expr.h.

◆ validate_expr() [4/25]

void validate_expr ( const dereference_exprt & value )

inline

Definition at line 876 of file pointer_expr.h.

◆ validate_expr() [5/25]

void validate_expr ( const dynamic_object_exprt & value )

inline

Definition at line 304 of file pointer_expr.h.

◆ validate_expr() [6/25]

void validate_expr ( const element_address_exprt & value )

inline

Definition at line 800 of file pointer_expr.h.

◆ validate_expr() [7/25]

void validate_expr ( const field_address_exprt & value )

inline

Definition at line 713 of file pointer_expr.h.

◆ validate_expr() [8/25]

void validate_expr ( const is_cstring_exprt & value )

inline

Definition at line 1480 of file pointer_expr.h.

◆ validate_expr() [9/25]

void validate_expr ( const is_dynamic_object_exprt & value )

inline

Definition at line 359 of file pointer_expr.h.

◆ validate_expr() [10/25]

void validate_expr ( const live_object_exprt & value )

inline

Definition at line 1594 of file pointer_expr.h.

◆ validate_expr() [11/25]

void validate_expr ( const object_address_exprt & value )

inline

Definition at line 629 of file pointer_expr.h.

◆ validate_expr() [12/25]

void validate_expr ( const object_descriptor_exprt & value )

inline

Definition at line 240 of file pointer_expr.h.

◆ validate_expr() [13/25]

void validate_expr ( const object_size_exprt & value )

inline

Definition at line 1443 of file pointer_expr.h.

◆ validate_expr() [14/25]

void validate_expr ( const pointer_in_range_exprt & value )

inline

Definition at line 426 of file pointer_expr.h.

◆ validate_expr() [15/25]

void validate_expr ( const pointer_object_exprt & value )

inline

Definition at line 1361 of file pointer_expr.h.

◆ validate_expr() [16/25]

void validate_expr ( const pointer_offset_exprt & value )

inline

Definition at line 1303 of file pointer_expr.h.

◆ validate_expr() [17/25]

void validate_expr ( const prophecy_pointer_in_range_exprt & value )

inline

Definition at line 508 of file pointer_expr.h.

◆ validate_expr() [18/25]

void validate_expr ( const prophecy_r_ok_exprt & value )

inline

Definition at line 1136 of file pointer_expr.h.

◆ validate_expr() [19/25]

void validate_expr ( const prophecy_r_or_w_ok_exprt & value )

inline

Definition at line 1086 of file pointer_expr.h.

◆ validate_expr() [20/25]

void validate_expr ( const prophecy_w_ok_exprt & value )

inline

Definition at line 1184 of file pointer_expr.h.

◆ validate_expr() [21/25]

void validate_expr ( const r_ok_exprt & value )

inline

Definition at line 971 of file pointer_expr.h.

◆ validate_expr() [22/25]

void validate_expr ( const r_or_w_ok_exprt & value )

inline

Definition at line 941 of file pointer_expr.h.

◆ validate_expr() [23/25]

void validate_expr ( const separate_exprt & value )

inline

Definition at line 1704 of file pointer_expr.h.

◆ validate_expr() [24/25]

void validate_expr ( const w_ok_exprt & value )

inline

Definition at line 1000 of file pointer_expr.h.

◆ validate_expr() [25/25]

void validate_expr ( const writeable_object_exprt & value )

inline

Definition at line 1650 of file pointer_expr.h.

Classes

Functions

Detailed Description

Function Documentation

◆ can_cast_expr< address_of_exprt >()

◆ can_cast_expr< annotated_pointer_constant_exprt >()

◆ can_cast_expr< cstrlen_exprt >()

◆ can_cast_expr< dereference_exprt >()

◆ can_cast_expr< dynamic_object_exprt >()

◆ can_cast_expr< element_address_exprt >()

◆ can_cast_expr< field_address_exprt >()

◆ can_cast_expr< is_cstring_exprt >()

◆ can_cast_expr< is_dynamic_object_exprt >()

◆ can_cast_expr< live_object_exprt >()

◆ can_cast_expr< object_address_exprt >()

◆ can_cast_expr< object_descriptor_exprt >()

◆ can_cast_expr< object_size_exprt >()

◆ can_cast_expr< pointer_in_range_exprt >()

◆ can_cast_expr< pointer_object_exprt >()

◆ can_cast_expr< pointer_offset_exprt >()

◆ can_cast_expr< prophecy_pointer_in_range_exprt >()

◆ can_cast_expr< prophecy_r_ok_exprt >()

◆ can_cast_expr< prophecy_r_or_w_ok_exprt >()

◆ can_cast_expr< prophecy_w_ok_exprt >()

◆ can_cast_expr< r_ok_exprt >()

◆ can_cast_expr< r_or_w_ok_exprt >()

◆ can_cast_expr< separate_exprt >()

◆ can_cast_expr< w_ok_exprt >()

◆ can_cast_expr< writeable_object_exprt >()

◆ can_cast_type< pointer_typet >()

◆ can_cast_type< reference_typet >()

◆ is_reference()

◆ is_rvalue_reference()

◆ is_void_pointer()

◆ to_address_of_expr() [1/2]

◆ to_address_of_expr() [2/2]

◆ to_annotated_pointer_constant_expr() [1/2]

◆ to_annotated_pointer_constant_expr() [2/2]

◆ to_cstrlen_expr() [1/2]

◆ to_cstrlen_expr() [2/2]

◆ to_dereference_expr() [1/2]

◆ to_dereference_expr() [2/2]

◆ to_dynamic_object_expr() [1/2]

◆ to_dynamic_object_expr() [2/2]

◆ to_element_address_expr() [1/2]

◆ to_element_address_expr() [2/2]

◆ to_field_address_expr() [1/2]

◆ to_field_address_expr() [2/2]

◆ to_is_cstring_expr() [1/2]

◆ to_is_cstring_expr() [2/2]

◆ to_is_dynamic_object_expr() [1/2]

◆ to_is_dynamic_object_expr() [2/2]

◆ to_live_object_expr() [1/2]

◆ to_live_object_expr() [2/2]

◆ to_object_address_expr() [1/2]

◆ to_object_address_expr() [2/2]

◆ to_object_descriptor_expr() [1/2]

◆ to_object_descriptor_expr() [2/2]

◆ to_object_size_expr() [1/2]

◆ to_object_size_expr() [2/2]

◆ to_pointer_in_range_expr() [1/2]

◆ to_pointer_in_range_expr() [2/2]

◆ to_pointer_object_expr() [1/2]

◆ to_pointer_object_expr() [2/2]

◆ to_pointer_offset_expr() [1/2]

◆ to_pointer_offset_expr() [2/2]

◆ to_pointer_type() [1/2]

◆ to_pointer_type() [2/2]

◆ to_prophecy_pointer_in_range_expr() [1/2]

◆ to_prophecy_pointer_in_range_expr() [2/2]

◆ to_prophecy_r_ok_expr()

◆ to_prophecy_r_or_w_ok_expr()

◆ to_prophecy_w_ok_expr()

◆ to_r_ok_expr()

◆ to_r_or_w_ok_expr()

◆ to_reference_type() [1/2]

◆ to_reference_type() [2/2]

◆ to_separate_expr() [1/2]

◆ to_separate_expr() [2/2]

◆ to_w_ok_expr()