CBMC
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
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_table_baset &_new_symbol_table, const optionst &_options, value_setst &_value_sets, message_handlert &message_handler)
 
void dereference_program (goto_programt &goto_program, bool checks_only=false)
 
void dereference_program (goto_functionst &goto_functions, bool checks_only=false)
 
void dereference_expression (const irep_idt &function_id, 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

const symbolt * get_or_create_failed_symbol (const exprt &expr) override
 
std::vector< exprt > get_value_set (const exprt &expr) const 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)
 Turn subexpression of expr of the form &*p into p and use dereference on subexpressions of the form *p More...
 
void dereference_expr (exprt &expr, const bool checks_only)
 Remove dereference expressions contained in expr. More...
 
- Protected Member Functions inherited from dereference_callbackt
virtual ~dereference_callbackt ()=default
 

Protected Attributes

const optionst & options
 
const namespacet & ns
 
value_setst & value_sets
 
value_set_dereferencet dereference
 
irep_idt current_function
 
goto_programt::const_targett current_target
 
goto_programt new_code
 

Detailed Description

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

Definition at line 29 of file goto_program_dereference.h.

Constructor & Destructor Documentation

◆ goto_program_dereferencet()

goto_program_dereferencet::goto_program_dereferencet ( const namespacet &  _ns,
symbol_table_baset &  _new_symbol_table,
const optionst &  _options,
value_setst &  _value_sets,
message_handlert &  message_handler 
)
inline

Definition at line 43 of file goto_program_dereference.h.

◆ ~goto_program_dereferencet()

virtual goto_program_dereferencet::~goto_program_dereferencet ( )
inlinevirtual

Definition at line 69 of file goto_program_dereference.h.

Member Function Documentation

◆ dereference_expr()

void goto_program_dereferencet::dereference_expr ( exprt &  expr,
const bool  checks_only 
)
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.

Definition at line 145 of file goto_program_dereference.cpp.

◆ dereference_expression()

void goto_program_dereferencet::dereference_expression ( const irep_idt &  function_id,
goto_programt::const_targett  target,
exprt &  expr 
)

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

Definition at line 247 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 195 of file goto_program_dereference.cpp.

◆ dereference_program() [1/2]

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

Definition at line 180 of file goto_program_dereference.cpp.

◆ dereference_program() [2/2]

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

Definition at line 158 of file goto_program_dereference.cpp.

◆ dereference_rec()

void goto_program_dereferencet::dereference_rec ( exprt &  expr)
protected

Turn subexpression of expr of the form &*p into p and use dereference on subexpressions of the form *p

Parameters
exprexpression in which to remove dereferences

Definition at line 50 of file goto_program_dereference.cpp.

◆ get_or_create_failed_symbol()

const symbolt * goto_program_dereferencet::get_or_create_failed_symbol ( const exprt &  expr)
overrideprotectedvirtual
Parameters
exprexpression to check
Returns
pointer to appropriate failed symbol for expr, or nullptr if none

Implements dereference_callbackt.

Definition at line 25 of file goto_program_dereference.cpp.

◆ get_value_set()

std::vector< exprt > goto_program_dereferencet::get_value_set ( const exprt &  expr) const
overrideprotectedvirtual

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

Parameters
expran expression
Returns
the value set

Implements dereference_callbackt.

Definition at line 135 of file goto_program_dereference.cpp.

Member Data Documentation

◆ current_function

irep_idt goto_program_dereferencet::current_function
protected

Definition at line 91 of file goto_program_dereference.h.

◆ current_target

goto_programt::const_targett goto_program_dereferencet::current_target
protected

Definition at line 92 of file goto_program_dereference.h.

◆ dereference

value_set_dereferencet goto_program_dereferencet::dereference
protected

Definition at line 77 of file goto_program_dereference.h.

◆ new_code

goto_programt goto_program_dereferencet::new_code
protected

Definition at line 93 of file goto_program_dereference.h.

◆ ns

const namespacet& goto_program_dereferencet::ns
protected

Definition at line 75 of file goto_program_dereference.h.

◆ options

const optionst& goto_program_dereferencet::options
protected

Definition at line 74 of file goto_program_dereference.h.

◆ value_sets

value_setst& goto_program_dereferencet::value_sets
protected

Definition at line 76 of file goto_program_dereference.h.

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