CBMC
pointer_expr.h File Reference

API to expression classes for Pointers. More...

#include "bitvector_types.h"
#include "std_expr.h"
+ Include dependency graph for pointer_expr.h:

Go to the source code of this file.

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  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  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. More...
 
const pointer_typetto_pointer_type (const typet &type)
 Cast a typet to a pointer_typet. More...
 
pointer_typetto_pointer_type (typet &type)
 Cast a typet to a pointer_typet. More...
 
bool is_void_pointer (const typet &type)
 This method tests, if the given typet is a pointer of type void. More...
 
template<>
bool can_cast_type< reference_typet > (const typet &type)
 Check whether a reference to a typet is a reference_typet. More...
 
const reference_typetto_reference_type (const typet &type)
 Cast a typet to a reference_typet. More...
 
reference_typetto_reference_type (typet &type)
 Cast a typet to a reference_typet. More...
 
bool is_reference (const typet &type)
 Returns true if the type is a reference. More...
 
bool is_rvalue_reference (const typet &type)
 Returns if the type is an R value reference. More...
 
template<>
bool can_cast_expr< object_descriptor_exprt > (const exprt &base)
 
void validate_expr (const object_descriptor_exprt &value)
 
const object_descriptor_exprtto_object_descriptor_expr (const exprt &expr)
 Cast an exprt to an object_descriptor_exprt. More...
 
object_descriptor_exprtto_object_descriptor_expr (exprt &expr)
 Cast an exprt to an object_descriptor_exprt. More...
 
template<>
bool can_cast_expr< dynamic_object_exprt > (const exprt &base)
 
void validate_expr (const dynamic_object_exprt &value)
 
const dynamic_object_exprtto_dynamic_object_expr (const exprt &expr)
 Cast an exprt to a dynamic_object_exprt. More...
 
dynamic_object_exprtto_dynamic_object_expr (exprt &expr)
 Cast an exprt to a dynamic_object_exprt. More...
 
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_exprtto_is_dynamic_object_expr (const exprt &expr)
 
is_dynamic_object_exprtto_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_exprtto_pointer_in_range_expr (const exprt &expr)
 
pointer_in_range_exprtto_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_exprtto_address_of_expr (const exprt &expr)
 Cast an exprt to an address_of_exprt. More...
 
address_of_exprtto_address_of_expr (exprt &expr)
 Cast an exprt to an address_of_exprt. More...
 
template<>
bool can_cast_expr< object_address_exprt > (const exprt &base)
 
void validate_expr (const object_address_exprt &value)
 
const object_address_exprtto_object_address_expr (const exprt &expr)
 Cast an exprt to an object_address_exprt. More...
 
object_address_exprtto_object_address_expr (exprt &expr)
 Cast an exprt to an object_address_exprt. More...
 
template<>
bool can_cast_expr< field_address_exprt > (const exprt &expr)
 
void validate_expr (const field_address_exprt &value)
 
const field_address_exprtto_field_address_expr (const exprt &expr)
 Cast an exprt to an field_address_exprt. More...
 
field_address_exprtto_field_address_expr (exprt &expr)
 Cast an exprt to an field_address_exprt. More...
 
template<>
bool can_cast_expr< element_address_exprt > (const exprt &expr)
 
void validate_expr (const element_address_exprt &value)
 
const element_address_exprtto_element_address_expr (const exprt &expr)
 Cast an exprt to an element_address_exprt. More...
 
element_address_exprtto_element_address_expr (exprt &expr)
 Cast an exprt to an element_address_exprt. More...
 
template<>
bool can_cast_expr< dereference_exprt > (const exprt &base)
 
void validate_expr (const dereference_exprt &value)
 
const dereference_exprtto_dereference_expr (const exprt &expr)
 Cast an exprt to a dereference_exprt. More...
 
dereference_exprtto_dereference_expr (exprt &expr)
 Cast an exprt to a dereference_exprt. More...
 
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_exprtto_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_exprtto_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_exprtto_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_exprtto_annotated_pointer_constant_expr (const exprt &expr)
 Cast an exprt to an annotated_pointer_constant_exprt. More...
 
annotated_pointer_constant_exprtto_annotated_pointer_constant_expr (exprt &expr)
 Cast an exprt to an annotated_pointer_constant_exprt. More...
 
template<>
bool can_cast_expr< pointer_offset_exprt > (const exprt &base)
 
void validate_expr (const pointer_offset_exprt &value)
 
const pointer_offset_exprtto_pointer_offset_expr (const exprt &expr)
 Cast an exprt to a pointer_offset_exprt. More...
 
pointer_offset_exprtto_pointer_offset_expr (exprt &expr)
 Cast an exprt to a pointer_offset_exprt. More...
 
template<>
bool can_cast_expr< pointer_object_exprt > (const exprt &base)
 
void validate_expr (const pointer_object_exprt &value)
 
const pointer_object_exprtto_pointer_object_expr (const exprt &expr)
 Cast an exprt to a pointer_object_exprt. More...
 
pointer_object_exprtto_pointer_object_expr (exprt &expr)
 Cast an exprt to a pointer_object_exprt. More...
 
const object_size_exprtto_object_size_expr (const exprt &expr)
 Cast an exprt to a object_size_exprt. More...
 
object_size_exprtto_object_size_expr (exprt &expr)
 Cast an exprt to a object_size_exprt. More...
 
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_exprtto_is_cstring_expr (const exprt &expr)
 Cast an exprt to a is_cstring_exprt. More...
 
is_cstring_exprtto_is_cstring_expr (exprt &expr)
 Cast an exprt to a is_cstring_exprt. More...
 
template<>
bool can_cast_expr< cstrlen_exprt > (const exprt &base)
 
void validate_expr (const cstrlen_exprt &value)
 
const cstrlen_exprtto_cstrlen_expr (const exprt &expr)
 Cast an exprt to a cstrlen_exprt. More...
 
cstrlen_exprtto_cstrlen_expr (exprt &expr)
 Cast an exprt to a cstrlen_exprt. More...
 
template<>
bool can_cast_expr< live_object_exprt > (const exprt &base)
 
void validate_expr (const live_object_exprt &value)
 
const live_object_exprtto_live_object_expr (const exprt &expr)
 Cast an exprt to a live_object_exprt. More...
 
live_object_exprtto_live_object_expr (exprt &expr)
 Cast an exprt to a live_object_exprt. More...
 
template<>
bool can_cast_expr< writeable_object_exprt > (const exprt &base)
 
void validate_expr (const writeable_object_exprt &value)
 
const writeable_object_exprtto_writeable_object_expr (const exprt &expr)
 Cast an exprt to a writeable_object_exprt. More...
 
writeable_object_exprtto_writeable_object_expr (exprt &expr)
 Cast an exprt to a writeable_object_exprt. More...
 
template<>
bool can_cast_expr< separate_exprt > (const exprt &base)
 
void validate_expr (const separate_exprt &value)
 
const separate_exprtto_separate_expr (const exprt &expr)
 Cast an exprt to a separate_exprt. More...
 
separate_exprtto_separate_expr (exprt &expr)
 Cast an exprt to a separate_exprt. More...
 

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 459 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 955 of file pointer_expr.h.

◆ can_cast_expr< cstrlen_exprt >()

template<>
bool can_cast_expr< cstrlen_exprt > ( const exprt base)
inline

Definition at line 1249 of file pointer_expr.h.

◆ can_cast_expr< dereference_exprt >()

template<>
bool can_cast_expr< dereference_exprt > ( const exprt base)
inline

Definition at line 772 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 285 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 696 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 609 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 1191 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 340 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 1305 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 525 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 221 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 1154 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 408 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 1072 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 1014 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 867 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 837 of file pointer_expr.h.

◆ can_cast_expr< separate_exprt >()

template<>
bool can_cast_expr< separate_exprt > ( const exprt base)
inline

Definition at line 1415 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 896 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 1361 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
typeSource type.
Returns
True if type is a pointer_typet.

Definition at line 66 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
typeSource type.
Returns
True if type is a reference_typet.

Definition at line 135 of file pointer_expr.h.

◆ is_reference()

bool is_reference ( const typet type)

Returns true if the type is a reference.

Definition at line 143 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 150 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 96 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
exprSource expression
Returns
Object of type address_of_exprt

Definition at line 475 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
exprSource expression
Returns
Object of type address_of_exprt

Definition at line 484 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
exprSource expression
Returns
Object of type annotated_pointer_constant_exprt

Definition at line 973 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
exprSource expression
Returns
Object of type annotated_pointer_constant_exprt

Definition at line 984 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
exprSource expression
Returns
Object of type cstrlen_exprt

Definition at line 1265 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
exprSource expression
Returns
Object of type cstrlen_exprt

Definition at line 1274 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
exprSource expression
Returns
Object of type dereference_exprt

Definition at line 788 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
exprSource expression
Returns
Object of type dereference_exprt

Definition at line 797 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
exprSource expression
Returns
Object of type dynamic_object_exprt

Definition at line 301 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
exprSource expression
Returns
Object of type dynamic_object_exprt

Definition at line 311 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
exprSource expression
Returns
Object of type element_address_exprt

Definition at line 712 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
exprSource expression
Returns
Object of type element_address_exprt

Definition at line 722 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
exprSource expression
Returns
Object of type field_address_exprt

Definition at line 625 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
exprSource expression
Returns
Object of type field_address_exprt

Definition at line 635 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
exprSource expression
Returns
Object of type is_cstring_exprt

Definition at line 1207 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
exprSource expression
Returns
Object of type is_cstring_exprt

Definition at line 1216 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 351 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 361 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
exprSource expression
Returns
Object of type live_object_exprt

Definition at line 1321 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
exprSource expression
Returns
Object of type live_object_exprt

Definition at line 1330 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
exprSource expression
Returns
Object of type object_address_exprt

Definition at line 541 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
exprSource expression
Returns
Object of type object_address_exprt

Definition at line 551 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
exprSource expression
Returns
Object of type object_descriptor_exprt

Definition at line 238 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
exprSource expression
Returns
Object of type object_descriptor_exprt

Definition at line 248 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
exprSource expression
Returns
Object of type object_size_exprt

Definition at line 1136 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
exprSource expression
Returns
Object of type object_size_exprt

Definition at line 1145 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 418 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 428 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
exprSource expression
Returns
Object of type pointer_object_exprt

Definition at line 1091 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
exprSource expression
Returns
Object of type pointer_object_exprt

Definition at line 1101 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
exprSource expression
Returns
Object of type pointer_offset_exprt

Definition at line 1033 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
exprSource expression
Returns
Object of type pointer_offset_exprt

Definition at line 1043 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
typeSource type.
Returns
Object of type pointer_typet.

Definition at line 79 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
typeSource type.
Returns
Object of type pointer_typet.

Definition at line 87 of file pointer_expr.h.

◆ to_r_ok_expr()

const r_ok_exprt& to_r_ok_expr ( const exprt expr)
inline

Definition at line 877 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 847 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
typeSource type.
Returns
Object of type reference_typet.

Definition at line 148 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
typeSource type.
Returns
Object of type reference_typet.

Definition at line 155 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
exprSource expression
Returns
Object of type separate_exprt

Definition at line 1430 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
exprSource expression
Returns
Object of type separate_exprt

Definition at line 1439 of file pointer_expr.h.

◆ to_w_ok_expr()

const w_ok_exprt& to_w_ok_expr ( const exprt expr)
inline

Definition at line 906 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
exprSource expression
Returns
Object of type writeable_object_exprt

Definition at line 1377 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
exprSource expression
Returns
Object of type writeable_object_exprt

Definition at line 1387 of file pointer_expr.h.

◆ validate_expr() [1/21]

void validate_expr ( const address_of_exprt value)
inline

Definition at line 464 of file pointer_expr.h.

◆ validate_expr() [2/21]

void validate_expr ( const annotated_pointer_constant_exprt value)
inline

Definition at line 960 of file pointer_expr.h.

◆ validate_expr() [3/21]

void validate_expr ( const cstrlen_exprt value)
inline

Definition at line 1254 of file pointer_expr.h.

◆ validate_expr() [4/21]

void validate_expr ( const dereference_exprt value)
inline

Definition at line 777 of file pointer_expr.h.

◆ validate_expr() [5/21]

void validate_expr ( const dynamic_object_exprt value)
inline

Definition at line 290 of file pointer_expr.h.

◆ validate_expr() [6/21]

void validate_expr ( const element_address_exprt value)
inline

Definition at line 701 of file pointer_expr.h.

◆ validate_expr() [7/21]

void validate_expr ( const field_address_exprt value)
inline

Definition at line 614 of file pointer_expr.h.

◆ validate_expr() [8/21]

void validate_expr ( const is_cstring_exprt value)
inline

Definition at line 1196 of file pointer_expr.h.

◆ validate_expr() [9/21]

void validate_expr ( const is_dynamic_object_exprt value)
inline

Definition at line 345 of file pointer_expr.h.

◆ validate_expr() [10/21]

void validate_expr ( const live_object_exprt value)
inline

Definition at line 1310 of file pointer_expr.h.

◆ validate_expr() [11/21]

void validate_expr ( const object_address_exprt value)
inline

Definition at line 530 of file pointer_expr.h.

◆ validate_expr() [12/21]

void validate_expr ( const object_descriptor_exprt value)
inline

Definition at line 226 of file pointer_expr.h.

◆ validate_expr() [13/21]

void validate_expr ( const object_size_exprt value)
inline

Definition at line 1159 of file pointer_expr.h.

◆ validate_expr() [14/21]

void validate_expr ( const pointer_in_range_exprt value)
inline

Definition at line 413 of file pointer_expr.h.

◆ validate_expr() [15/21]

void validate_expr ( const pointer_object_exprt value)
inline

Definition at line 1077 of file pointer_expr.h.

◆ validate_expr() [16/21]

void validate_expr ( const pointer_offset_exprt value)
inline

Definition at line 1019 of file pointer_expr.h.

◆ validate_expr() [17/21]

void validate_expr ( const r_ok_exprt value)
inline

Definition at line 872 of file pointer_expr.h.

◆ validate_expr() [18/21]

void validate_expr ( const r_or_w_ok_exprt value)
inline

Definition at line 842 of file pointer_expr.h.

◆ validate_expr() [19/21]

void validate_expr ( const separate_exprt value)
inline

Definition at line 1420 of file pointer_expr.h.

◆ validate_expr() [20/21]

void validate_expr ( const w_ok_exprt value)
inline

Definition at line 901 of file pointer_expr.h.

◆ validate_expr() [21/21]

void validate_expr ( const writeable_object_exprt value)
inline

Definition at line 1366 of file pointer_expr.h.