cprover
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  address_of_exprt
 Operator to return the address of an object. 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. 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...
 

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...
 
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< 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< 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...
 
const r_or_w_ok_exprtto_r_or_w_ok_expr (const exprt &expr)
 
const r_ok_exprtto_r_ok_expr (const exprt &expr)
 
const w_ok_exprtto_w_ok_expr (const exprt &expr)
 

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

◆ can_cast_expr< dereference_exprt >()

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

Definition at line 426 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 265 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 201 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 49 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 115 of file pointer_expr.h.

◆ is_reference()

bool is_reference ( const typet type)

Returns true if the type is a reference.

Definition at line 133 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 140 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 79 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 367 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 376 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 442 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 451 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 281 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 291 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 310 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 320 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 218 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 228 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 62 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 70 of file pointer_expr.h.

◆ to_r_ok_expr()

const r_ok_exprt& to_r_ok_expr ( const exprt expr)
inline

Definition at line 508 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 490 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 128 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 135 of file pointer_expr.h.

◆ to_w_ok_expr()

const w_ok_exprt& to_w_ok_expr ( const exprt expr)
inline

Definition at line 526 of file pointer_expr.h.

◆ validate_expr() [1/4]

void validate_expr ( const address_of_exprt value)
inline

Definition at line 356 of file pointer_expr.h.

◆ validate_expr() [2/4]

void validate_expr ( const dereference_exprt value)
inline

Definition at line 431 of file pointer_expr.h.

◆ validate_expr() [3/4]

void validate_expr ( const dynamic_object_exprt value)
inline

Definition at line 270 of file pointer_expr.h.

◆ validate_expr() [4/4]

void validate_expr ( const object_descriptor_exprt value)
inline

Definition at line 206 of file pointer_expr.h.