cprover
goto_program_dereferencet Class Reference

Wrapper for functions removing dereferences in expressions contained in a goto program. More...

#include <goto_program_dereference.h>

+ Inheritance diagram for goto_program_dereferencet:
+ Collaboration diagram for goto_program_dereferencet:

Public Member Functions

 goto_program_dereferencet (const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, value_setst &_value_sets)
 
void dereference_program (goto_programt &goto_program, bool checks_only=false)
 
void dereference_program (goto_functionst &goto_functions, bool checks_only=false)
 
void pointer_checks (goto_programt &goto_program)
 Throw an exception in case removing dereferences from the program would throw an exception. More...
 
void pointer_checks (goto_functionst &goto_functions)
 Throw an exception in case removing dereferences from the program would throw an exception. More...
 
void dereference_expression (goto_programt::const_targett target, exprt &expr)
 Set the current target to target and remove derefence from expr. More...
 
virtual ~goto_program_dereferencet ()
 

Protected Member Functions

virtual bool is_valid_object (const irep_idt &identifier)
 
bool has_failed_symbol (const exprt &expr, const symbolt *&symbol) override
 
virtual void dereference_failure (const std::string &property, const std::string &msg, const guardt &guard)
 
void get_value_set (const exprt &expr, value_setst::valuest &dest) override
 Gets the value set corresponding to the current target and expression expr. More...
 
void dereference_instruction (goto_programt::targett target, bool checks_only=false)
 Remove dereference from expressions contained in the instruction at target. More...
 
void dereference_rec (exprt &expr, guardt &guard, const value_set_dereferencet::modet mode)
 Turn subexpression of expr of the form &*p or reference_to(*p) to p and use dereference on subexpressions of the form *p More...
 
void dereference_expr (exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
 Remove dereference expressions contained in expr. More...
 
- Protected Member Functions inherited from dereference_callbackt
virtual ~dereference_callbackt ()=default
 

Protected Attributes

const optionstoptions
 
const namespacetns
 
value_setstvalue_sets
 
value_set_dereferencet dereference
 
goto_programt::const_targett current_target
 
source_locationt dereference_location
 Unused. More...
 
std::set< exprtassertions
 Unused. More...
 
goto_programt new_code
 Unused. More...
 

Detailed Description

Wrapper for functions removing dereferences in expressions contained in a goto program.

Definition at line 24 of file goto_program_dereference.h.

Constructor & Destructor Documentation

◆ goto_program_dereferencet()

goto_program_dereferencet::goto_program_dereferencet ( const namespacet _ns,
symbol_tablet _new_symbol_table,
const optionst _options,
value_setst _value_sets 
)
inline

Definition at line 31 of file goto_program_dereference.h.

◆ ~goto_program_dereferencet()

virtual goto_program_dereferencet::~goto_program_dereferencet ( )
inlinevirtual

Definition at line 58 of file goto_program_dereference.h.

Member Function Documentation

◆ dereference_expr()

void goto_program_dereferencet::dereference_expr ( exprt expr,
const bool  checks_only,
const value_set_dereferencet::modet  mode 
)
protected

Remove dereference expressions contained in expr.

Parameters
expran expression
checks_onlywhen true, execute the substitution on a copy of expr so that expr stays unchanged. In that case the only observable effect is whether an exception would be thrown.
modeunused

Definition at line 250 of file goto_program_dereference.cpp.

◆ dereference_expression()

void goto_program_dereferencet::dereference_expression ( goto_programt::const_targett  target,
exprt expr 
)

Set the current target to target and remove derefence from expr.

Definition at line 371 of file goto_program_dereference.cpp.

◆ dereference_failure()

void goto_program_dereferencet::dereference_failure ( const std::string &  property,
const std::string &  msg,
const guardt guard 
)
protectedvirtual
Deprecated:

Definition at line 70 of file goto_program_dereference.cpp.

◆ dereference_instruction()

void goto_program_dereferencet::dereference_instruction ( goto_programt::targett  target,
bool  checks_only = false 
)
protected

Remove dereference from expressions contained in the instruction at target.

If check_only is true, the dereferencing is performed on copies of the expressions, in that case the only observable effect is whether an exception would be thrown.

Definition at line 305 of file goto_program_dereference.cpp.

◆ dereference_program() [1/2]

void goto_program_dereferencet::dereference_program ( goto_programt goto_program,
bool  checks_only = false 
)

Definition at line 266 of file goto_program_dereference.cpp.

◆ dereference_program() [2/2]

void goto_program_dereferencet::dereference_program ( goto_functionst goto_functions,
bool  checks_only = false 
)

Definition at line 290 of file goto_program_dereference.cpp.

◆ dereference_rec()

void goto_program_dereferencet::dereference_rec ( exprt expr,
guardt guard,
const value_set_dereferencet::modet  mode 
)
protected

Turn subexpression of expr of the form &*p or reference_to(*p) to p and use dereference on subexpressions of the form *p

Parameters
exprexpression in which to remove dereferences
guardboolean expression assumed to hold when dereferencing
modeunused

Definition at line 104 of file goto_program_dereference.cpp.

◆ get_value_set()

void goto_program_dereferencet::get_value_set ( const exprt expr,
value_setst::valuest dest 
)
overrideprotectedvirtual

Gets the value set corresponding to the current target and expression expr.

Parameters
expran expression
[out]destgets the value set

Implements dereference_callbackt.

Definition at line 237 of file goto_program_dereference.cpp.

◆ has_failed_symbol()

bool goto_program_dereferencet::has_failed_symbol ( const exprt expr,
const symbolt *&  symbol 
)
overrideprotectedvirtual
Parameters
exprexpression to check
[out]symbolsymbol which gets assigned the value from the failed_symbol comment
Returns
true when expr is a symbol, whose type contains a failed_symbol comment which exists in the namespace.

Implements dereference_callbackt.

Definition at line 27 of file goto_program_dereference.cpp.

◆ is_valid_object()

bool goto_program_dereferencet::is_valid_object ( const irep_idt identifier)
protectedvirtual
Deprecated:

Definition at line 50 of file goto_program_dereference.cpp.

◆ pointer_checks() [1/2]

void goto_program_dereferencet::pointer_checks ( goto_programt goto_program)

Throw an exception in case removing dereferences from the program would throw an exception.

Definition at line 385 of file goto_program_dereference.cpp.

◆ pointer_checks() [2/2]

void goto_program_dereferencet::pointer_checks ( goto_functionst goto_functions)

Throw an exception in case removing dereferences from the program would throw an exception.

Definition at line 393 of file goto_program_dereference.cpp.

Member Data Documentation

◆ assertions

std::set<exprt> goto_program_dereferencet::assertions
protected

Unused.

Definition at line 102 of file goto_program_dereference.h.

◆ current_target

goto_programt::const_targett goto_program_dereferencet::current_target
protected

Definition at line 96 of file goto_program_dereference.h.

◆ dereference

value_set_dereferencet goto_program_dereferencet::dereference
protected

Definition at line 66 of file goto_program_dereference.h.

◆ dereference_location

source_locationt goto_program_dereferencet::dereference_location
protected

Unused.

Definition at line 99 of file goto_program_dereference.h.

◆ new_code

goto_programt goto_program_dereferencet::new_code
protected

Unused.

Definition at line 105 of file goto_program_dereference.h.

◆ ns

const namespacet& goto_program_dereferencet::ns
protected

Definition at line 64 of file goto_program_dereference.h.

◆ options

const optionst& goto_program_dereferencet::options
protected

Definition at line 63 of file goto_program_dereference.h.

◆ value_sets

value_setst& goto_program_dereferencet::value_sets
protected

Definition at line 65 of file goto_program_dereference.h.


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