cprover
Public Member Functions | Private Member Functions | Private Attributes | List of all members
dereferencet Class Reference

Wrapper for a function which dereference a pointer-expression. More...

#include <dereference.h>

+ Collaboration diagram for dereferencet:

Public Member Functions

 dereferencet (const namespacet &_ns)
 
 ~dereferencet ()
 
exprt operator() (const exprt &pointer)
 Dereference the given pointer-expression. More...
 

Private Member Functions

exprt dereference_rec (const exprt &address, const exprt &offset, const typet &type)
 Attempt to dereference the object at address address + offset and of type type. More...
 
exprt dereference_if (const if_exprt &expr, const exprt &offset, const typet &type)
 Attempt to dereference the object at address expr + offset and of type type. More...
 
exprt dereference_plus (const exprt &expr, const exprt &offset, const typet &type)
 Attempt to dereference the object at address expr + offset and of type type. More...
 
exprt dereference_typecast (const typecast_exprt &expr, const exprt &offset, const typet &type)
 Attempt to dereference the object at address expr + offset and of type type. More...
 
bool type_compatible (const typet &object_type, const typet &dereference_type) const
 Check that it is ok to cast an object of type object_type to deference_type. More...
 
exprt read_object (const exprt &object, const exprt &offset, const typet &type)
 

Private Attributes

const namespacet & ns
 

Detailed Description

Wrapper for a function which dereference a pointer-expression.

Definition at line 22 of file dereference.h.

Constructor & Destructor Documentation

◆ dereferencet()

dereferencet::dereferencet ( const namespacet &  _ns)
inlineexplicit

Definition at line 25 of file dereference.h.

◆ ~dereferencet()

dereferencet::~dereferencet ( )
inline

Definition at line 31 of file dereference.h.

Member Function Documentation

◆ dereference_if()

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

Attempt to dereference the object at address expr + offset and of type type.

Throws an exception if unsuccessful.

This is done by dereferencing both the true and false cases of the if expression and putting the result together in a new if expression with the same condition.

Returns
the dereferenced object

Definition at line 218 of file dereference.cpp.

◆ dereference_plus()

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

Attempt to dereference the object at address expr + offset and of type type.

Throws an exception if unsuccessful. This assumes expr is a plus_exprt but does not check for it.

Definition at line 233 of file dereference.cpp.

◆ dereference_rec()

exprt dereferencet::dereference_rec ( const exprt &  address,
const exprt &  offset,
const typet &  type 
)
private

Attempt to dereference the object at address address + offset and of type type.

Throws an exception if unsuccessful.

Definition at line 157 of file dereference.cpp.

◆ dereference_typecast()

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

Attempt to dereference the object at address expr + offset and of type type.

Throws an exception if unsuccessful.

If expr is a typecast of the form (type)ptr:

  • if ptr is of pointer type, dereference ptr + offset
  • if ptr is of integer type, return an integer_dereference expression
  • otherwise throw an exception
    Returns
    The dereferenced object.

Definition at line 276 of file dereference.cpp.

◆ operator()()

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

Dereference the given pointer-expression.

Parameters
pointerA pointer-typed expression, to be dereferenced.
Returns
Object after dereferencing.

Definition at line 28 of file dereference.cpp.

◆ read_object()

exprt dereferencet::read_object ( const exprt &  object,
const exprt &  offset,
const typet &  type 
)
private
Returns
Expression equivalent to byte_extract(object, offset) and of type type. The expression is potentially simplified so that for instance in the case of an array, object[offset] can be returned.

Definition at line 50 of file dereference.cpp.

◆ type_compatible()

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

Check that it is ok to cast an object of type object_type to deference_type.

Definition at line 307 of file dereference.cpp.

Member Data Documentation

◆ ns

const namespacet& dereferencet::ns
private

Definition at line 39 of file dereference.h.

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