cprover
pointer_expr.h File Reference

API to expression classes for Pointers. More...

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

Go to the source code of this file.

Classes

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...
 

Functions

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...
 

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

◆ can_cast_expr< dereference_exprt >()

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

Definition at line 296 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 135 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 71 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 237 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 246 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 312 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 321 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 151 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 161 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 180 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 190 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 88 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 98 of file pointer_expr.h.

◆ validate_expr() [1/4]

void validate_expr ( const address_of_exprt value)
inline

Definition at line 226 of file pointer_expr.h.

◆ validate_expr() [2/4]

void validate_expr ( const dereference_exprt value)
inline

Definition at line 301 of file pointer_expr.h.

◆ validate_expr() [3/4]

void validate_expr ( const dynamic_object_exprt value)
inline

Definition at line 140 of file pointer_expr.h.

◆ validate_expr() [4/4]

void validate_expr ( const object_descriptor_exprt value)
inline

Definition at line 76 of file pointer_expr.h.