CBMC
value_set_dereferencet Class Referencefinal

Wrapper for a function dereferencing pointer expressions using a value set. More...

#include <value_set_dereference.h>

+ Collaboration diagram for value_set_dereferencet:

Classes

class  valuet
 Return value for build_reference_to; see that method for documentation. More...
 

Public Member Functions

 value_set_dereferencet (const namespacet &_ns, symbol_table_baset &_new_symbol_table, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs, message_handlert &_message_handler)
 
virtual ~value_set_dereferencet ()
 
exprt dereference (const exprt &pointer, bool display_points_to_sets=false)
 Dereference the given pointer-expression. More...
 

Static Public Member Functions

static bool should_ignore_value (const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
 Determine whether possible alias what should be ignored when replacing a pointer by its referees. More...
 
static valuet build_reference_to (const exprt &what, const exprt &pointer, const namespacet &ns)
 
static bool dereference_type_compare (const typet &object_type, const typet &dereference_type, const namespacet &ns)
 Check if the two types have matching number of ID_pointer levels, with the dereference type eventually pointing to void; then this is ok for example: More...
 
static bool memory_model (exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
 Replace value by an expression of type to_type corresponding to the value at memory address value + offset. More...
 
static bool memory_model_bytes (exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
 Replace value by an expression of type to_type corresponding to the value at memory address value + offset. More...
 

Private Member Functions

valuet get_failure_value (const exprt &pointer, const typet &type)
 
exprt handle_dereference_base_case (const exprt &pointer, bool display_points_to_sets)
 

Private Attributes

const namespacetns
 
symbol_table_basetnew_symbol_table
 
dereference_callbacktdereference_callback
 
const irep_idt language_mode
 language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise. More...
 
const bool exclude_null_derefs
 Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to dereference NULL. More...
 
message_handlertmessage_handler
 

Detailed Description

Wrapper for a function dereferencing pointer expressions using a value set.

Definition at line 22 of file value_set_dereference.h.

Constructor & Destructor Documentation

◆ value_set_dereferencet()

value_set_dereferencet::value_set_dereferencet ( const namespacet _ns,
symbol_table_baset _new_symbol_table,
dereference_callbackt _dereference_callback,
const irep_idt  _language_mode,
bool  _exclude_null_derefs,
message_handlert _message_handler 
)
inline
Parameters
_nsNamespace
_new_symbol_tableA symbol_table to store new symbols in
_dereference_callbackCallback object for getting the set of objects a given pointer may point to.
_language_modeMode for any new symbols created to represent a dereference failure
_exclude_null_derefsIgnore value-set entries that indicate a
_message_handlerMessage handler for displaying points-to set

Definition at line 34 of file value_set_dereference.h.

◆ ~value_set_dereferencet()

virtual value_set_dereferencet::~value_set_dereferencet ( )
inlinevirtual

Definition at line 49 of file value_set_dereference.h.

Member Function Documentation

◆ build_reference_to()

value_set_dereferencet::valuet value_set_dereferencet::build_reference_to ( const exprt what,
const exprt pointer_expr,
const namespacet ns 
)
static
Parameters
whatvalue set entry to convert to an expression: either ID_unknown, ID_invalid, or an object_descriptor_exprt giving a referred object and offset.
pointer_exprpointer expression that may point to what
nsA namespace
Returns
a valuet object containing guard and value fields. The guard is an appropriate check to determine whether pointer_expr really points to what; for example pointer_expr == &what. The value corresponds to the dereferenced pointer_expr assuming it is pointing to the object described by what. For example, we might return {.value = global, .pointer_guard = (pointer_expr == &global)}

Definition at line 459 of file value_set_dereference.cpp.

◆ dereference()

exprt value_set_dereferencet::dereference ( const exprt pointer,
bool  display_points_to_sets = false 
)

Dereference the given pointer-expression.

Any errors are reported to the callback method given in the constructor.

Parameters
pointerA pointer-typed expression, to be dereferenced.
display_points_to_setsDisplay size and contents of points to sets

Definition at line 143 of file value_set_dereference.cpp.

◆ dereference_type_compare()

bool value_set_dereferencet::dereference_type_compare ( const typet object_type,
const typet dereference_type,
const namespacet ns 
)
static

Check if the two types have matching number of ID_pointer levels, with the dereference type eventually pointing to void; then this is ok for example:

  • dereference_type=void is ok (no matter what object_type is);
  • object_type=(int *), dereference_type=(void *) is ok;
  • object_type=(int **), dereference_type=(void **) is ok;
  • object_type=(int **), dereference_type=(void *) is ok;
  • object_type=(int *), dereference_type=(void **) is not ok;

Definition at line 340 of file value_set_dereference.cpp.

◆ get_failure_value()

value_set_dereferencet::valuet value_set_dereferencet::get_failure_value ( const exprt pointer,
const typet type 
)
private

Definition at line 293 of file value_set_dereference.cpp.

◆ handle_dereference_base_case()

exprt value_set_dereferencet::handle_dereference_base_case ( const exprt pointer,
bool  display_points_to_sets 
)
private

Definition at line 215 of file value_set_dereference.cpp.

◆ memory_model()

bool value_set_dereferencet::memory_model ( exprt value,
const typet to_type,
const exprt offset,
const namespacet ns 
)
static

Replace value by an expression of type to_type corresponding to the value at memory address value + offset.

If value is a bitvector or pointer of the same size as to_type, make value into the typecast expression (to_type)value. Otherwise perform the same operation as value_set_dereferencet::memory_model_bytes

Returns
true on success

Definition at line 707 of file value_set_dereference.cpp.

◆ memory_model_bytes()

bool value_set_dereferencet::memory_model_bytes ( exprt value,
const typet to_type,
const exprt offset,
const namespacet ns 
)
static

Replace value by an expression of type to_type corresponding to the value at memory address value + offset.

If the type of value is an array of bitvectors of size 1 byte, and to_type also is bitvector of size 1 byte, then the resulting expression is value[offset] or (to_type)value[offset] when typecast is required. Otherwise the expression is byte_extract(value, offset).

Returns
false if the conversion cannot be made

Definition at line 754 of file value_set_dereference.cpp.

◆ should_ignore_value()

bool value_set_dereferencet::should_ignore_value ( const exprt what,
bool  exclude_null_derefs,
const irep_idt language_mode 
)
static

Determine whether possible alias what should be ignored when replacing a pointer by its referees.

We currently ignore a null object when exclude_null_derefs is true (pass true if you know the dereferenced pointer cannot be null), and also ignore integer addresses when language_mode is "java"

Parameters
whatvalue set entry to convert to an expression: either ID_unknown, ID_invalid, or an object_descriptor_exprt giving a referred object and offset.
exclude_null_derefsIgnore value-set entries that indicate a given dereference may follow a null pointer
language_modeMode for any new symbols created to represent a dereference failure
Returns
true if what should be ignored as a possible alias

Definition at line 422 of file value_set_dereference.cpp.

Member Data Documentation

◆ dereference_callback

dereference_callbackt& value_set_dereferencet::dereference_callback
private

Definition at line 101 of file value_set_dereference.h.

◆ exclude_null_derefs

const bool value_set_dereferencet::exclude_null_derefs
private

Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to dereference NULL.

Definition at line 107 of file value_set_dereference.h.

◆ language_mode

const irep_idt value_set_dereferencet::language_mode
private

language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.

Definition at line 104 of file value_set_dereference.h.

◆ message_handler

message_handlert& value_set_dereferencet::message_handler
private

Definition at line 108 of file value_set_dereference.h.

◆ new_symbol_table

symbol_table_baset& value_set_dereferencet::new_symbol_table
private

Definition at line 100 of file value_set_dereference.h.

◆ ns

const namespacet& value_set_dereferencet::ns
private

Definition at line 99 of file value_set_dereference.h.


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