cprover
value_set_dereferencet Class Reference

TO_BE_DOCUMENTED. More...

#include <value_set_dereference.h>

Collaboration diagram for value_set_dereferencet:
[legend]

Classes

class  valuet
 

Public Types

enum  modet { modet::READ, modet::WRITE }
 
typedef std::unordered_set< exprt, irep_hashexpr_sett
 

Public Member Functions

 value_set_dereferencet (const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, dereference_callbackt &_dereference_callback, const irep_idt _language_mode)
 Constructor. More...
 
virtual ~value_set_dereferencet ()
 
virtual exprt dereference (const exprt &pointer, const guardt &guard, const modet mode)
 

Static Public Member Functions

static bool has_dereference (const exprt &expr)
 Returns 'true' iff the given expression contains unary '*'. More...
 

Private Member Functions

bool dereference_type_compare (const typet &object_type, const typet &dereference_type) const
 
void offset_sum (exprt &dest, const exprt &offset) const
 
valuet build_reference_to (const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
 
bool get_value_guard (const exprt &symbol, const exprt &premise, exprt &value)
 
void bounds_check (const index_exprt &expr, const guardt &guard)
 
void valid_check (const exprt &expr, const guardt &guard, const modet mode)
 
void invalid_pointer (const exprt &expr, const guardt &guard)
 
bool memory_model (exprt &value, const typet &type, const guardt &guard, const exprt &offset)
 
bool memory_model_conversion (exprt &value, const typet &type, const guardt &guard, const exprt &offset)
 
bool memory_model_bytes (exprt &value, const typet &type, const guardt &guard, const exprt &offset)
 

Static Private Member Functions

static const exprtget_symbol (const exprt &object)
 

Private Attributes

const namespacetns
 
symbol_tabletnew_symbol_table
 
const optionstoptions
 
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...
 

Static Private Attributes

static unsigned invalid_counter =0
 

Detailed Description

TO_BE_DOCUMENTED.

Definition at line 29 of file value_set_dereference.h.

Member Typedef Documentation

§ expr_sett

typedef std::unordered_set<exprt, irep_hash> value_set_dereferencet::expr_sett

Definition at line 79 of file value_set_dereference.h.

Member Enumeration Documentation

§ modet

Enumerator
READ 
WRITE 

Definition at line 54 of file value_set_dereference.h.

Constructor & Destructor Documentation

§ value_set_dereferencet()

value_set_dereferencet::value_set_dereferencet ( const namespacet _ns,
symbol_tablet _new_symbol_table,
const optionst _options,
dereference_callbackt _dereference_callback,
const irep_idt  _language_mode 
)
inline

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 39 of file value_set_dereference.h.

§ ~value_set_dereferencet()

virtual value_set_dereferencet::~value_set_dereferencet ( )
inlinevirtual

Definition at line 52 of file value_set_dereference.h.

Member Function Documentation

§ bounds_check()

§ build_reference_to()

value_set_dereferencet::valuet value_set_dereferencet::build_reference_to ( const exprt what,
const modet  mode,
const exprt pointer,
const guardt guard 
)
private

§ dereference()

exprt value_set_dereferencet::dereference ( const exprt pointer,
const guardt guard,
const modet  mode 
)
virtual

The method 'dereference' dereferences the given pointer-expression. Any errors are reported to the callback method given in the constructor.

Parameters
pointerA pointer-typed expression, to be dereferenced.
guardA guard, which is assumed to hold when dereferencing.
modeIndicates whether the dereferencing is a load or store.
parameters: expression dest, to be dereferenced under given guard,
and given mode
Returns
returns pointer after dereferencing

Definition at line 66 of file value_set_dereference.cpp.

References guardt::add(), symbolt::base_name, build_reference_to(), if_exprt::cond(), dereference_callback, if_exprt::false_case(), from_expr(), get_new_name(), dereference_callbackt::get_value_set(), dereference_callbackt::has_failed_symbol(), irept::id(), invalid_counter, invalid_pointer(), symbolt::is_lvalue, irept::is_nil(), symbol_tablet::move(), symbolt::name, new_symbol_table, ns, value_set_dereferencet::valuet::pointer_guard, irept::pretty(), irept::set(), typet::subtype(), symbolt::symbol_expr(), to_if_expr(), if_exprt::true_case(), symbolt::type, exprt::type(), and value_set_dereferencet::valuet::value.

Referenced by goto_program_dereferencet::dereference_rec(), and goto_symext::dereference_rec().

§ dereference_type_compare()

bool value_set_dereferencet::dereference_type_compare ( const typet object_type,
const typet dereference_type 
) const
private

§ get_symbol()

const exprt & value_set_dereferencet::get_symbol ( const exprt object)
staticprivate

Definition at line 55 of file value_set_dereference.cpp.

References irept::id(), and exprt::op0().

Referenced by valid_check(), and value_set_dereferencet::valuet::valuet().

§ get_value_guard()

bool value_set_dereferencet::get_value_guard ( const exprt symbol,
const exprt premise,
exprt value 
)
private

§ has_dereference()

bool value_set_dereferencet::has_dereference ( const exprt expr)
static

Returns 'true' iff the given expression contains unary '*'.

Definition at line 50 of file value_set_dereference.cpp.

References has_subexpr().

Referenced by goto_program_dereferencet::dereference_rec(), and rw_range_set_value_sett::get_objects_dereference().

§ invalid_pointer()

void value_set_dereferencet::invalid_pointer ( const exprt expr,
const guardt guard 
)
private

§ memory_model()

bool value_set_dereferencet::memory_model ( exprt value,
const typet type,
const guardt guard,
const exprt offset 
)
private

§ memory_model_bytes()

§ memory_model_conversion()

bool value_set_dereferencet::memory_model_conversion ( exprt value,
const typet type,
const guardt guard,
const exprt offset 
)
private

§ offset_sum()

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

§ valid_check()

Member Data Documentation

§ dereference_callback

dereference_callbackt& value_set_dereferencet::dereference_callback
private

§ invalid_counter

unsigned int value_set_dereferencet::invalid_counter =0
staticprivate

Definition at line 89 of file value_set_dereference.h.

Referenced by dereference().

§ 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 88 of file value_set_dereference.h.

Referenced by build_reference_to().

§ new_symbol_table

symbol_tablet& value_set_dereferencet::new_symbol_table
private

Definition at line 83 of file value_set_dereference.h.

Referenced by dereference().

§ ns

§ options

const optionst& value_set_dereferencet::options
private

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