cprover
dereferencet Class Reference

TO_BE_DOCUMENTED. More...

#include <dereference.h>

Collaboration diagram for dereferencet:
[legend]

Public Member Functions

 dereferencet (const namespacet &_ns)
 Constructor. More...
 
 ~dereferencet ()
 
exprt operator() (const exprt &pointer)
 

Private Member Functions

exprt dereference_rec (const exprt &address, const exprt &offset, const typet &type)
 
exprt dereference_if (const if_exprt &expr, const exprt &offset, const typet &type)
 
exprt dereference_plus (const exprt &expr, const exprt &offset, const typet &type)
 
exprt dereference_typecast (const typecast_exprt &expr, const exprt &offset, const typet &type)
 
bool type_compatible (const typet &object_type, const typet &dereference_type) const
 
void offset_sum (exprt &dest, const exprt &offset) const
 
exprt read_object (const exprt &object, const exprt &offset, const typet &type)
 

Private Attributes

const namespacetns
 

Detailed Description

TO_BE_DOCUMENTED.

Definition at line 23 of file dereference.h.

Constructor & Destructor Documentation

§ dereferencet()

dereferencet::dereferencet ( const namespacet _ns)
inlineexplicit

Constructor.

Parameters
_nsNamespace
_new_symbol_tableA symbol_table to store new symbols in
_optionsOptions, in particular whether pointer checks are to be performed
_dereference_callbackCallback object for error reporting

Definition at line 33 of file dereference.h.

§ ~dereferencet()

dereferencet::~dereferencet ( )
inline

Definition at line 39 of file dereference.h.

References operator()().

Member Function Documentation

§ dereference_if()

exprt dereferencet::dereference_if ( const if_exprt expr,
const exprt offset,
const typet type 
)
private

§ dereference_plus()

exprt dereferencet::dereference_plus ( const exprt expr,
const exprt offset,
const typet type 
)
private

§ dereference_rec()

§ dereference_typecast()

exprt dereferencet::dereference_typecast ( const typecast_exprt expr,
const exprt offset,
const typet type 
)
private

§ offset_sum()

void dereferencet::offset_sum ( exprt dest,
const exprt offset 
) const
private

§ operator()()

exprt dereferencet::operator() ( const exprt pointer)

The operator '()' dereferences the given pointer-expression.

Parameters
pointerA pointer-typed expression, to be dereferenced.
parameters: expression, to be dereferenced
Returns
returns object after dereferencing

Definition at line 30 of file dereference.cpp.

References dereference_rec(), from_expr(), from_integer(), irept::id(), index_type(), ns, irept::pretty(), typet::subtype(), and exprt::type().

Referenced by ~dereferencet().

§ read_object()

§ type_compatible()

bool dereferencet::type_compatible ( const typet object_type,
const typet dereference_type 
) const
private

Member Data Documentation

§ ns

const namespacet& dereferencet::ns
private

The documentation for this class was generated from the following files: