cprover
goto_program_dereferencet Class Reference

#include <goto_program_dereference.h>

Inheritance diagram for goto_program_dereferencet:
[legend]
Collaboration diagram for goto_program_dereferencet:
[legend]

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)
 
void pointer_checks (goto_functionst &goto_functions)
 
void dereference_expression (goto_programt::const_targett target, exprt &expr)
 
virtual ~goto_program_dereferencet ()
 

Protected Member Functions

virtual bool is_valid_object (const irep_idt &identifier)
 
virtual bool has_failed_symbol (const exprt &expr, const symbolt *&symbol)
 
virtual void dereference_failure (const std::string &property, const std::string &msg, const guardt &guard)
 
virtual void get_value_set (const exprt &expr, value_setst::valuest &dest)
 
void dereference_instruction (goto_programt::targett target, bool checks_only=false)
 
void dereference_rec (exprt &expr, guardt &guard, const value_set_dereferencet::modet mode)
 
void dereference_expr (exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
 
- Protected Member Functions inherited from dereference_callbackt
virtual ~dereference_callbackt ()
 

Protected Attributes

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

Detailed Description

Definition at line 22 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 29 of file goto_program_dereference.h.

◆ ~goto_program_dereferencet()

virtual goto_program_dereferencet::~goto_program_dereferencet ( )
inlinevirtual

Definition at line 54 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

Definition at line 238 of file goto_program_dereference.cpp.

References dereference_rec().

Referenced by dereference_expression(), and dereference_instruction().

◆ dereference_expression()

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

◆ dereference_failure()

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

◆ dereference_instruction()

◆ dereference_program() [1/2]

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

◆ dereference_program() [2/2]

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

◆ dereference_rec()

◆ get_value_set()

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

◆ has_failed_symbol()

bool goto_program_dereferencet::has_failed_symbol ( const exprt expr,
const symbolt *&  symbol 
)
protectedvirtual

◆ is_valid_object()

bool goto_program_dereferencet::is_valid_object ( const irep_idt identifier)
protectedvirtual

◆ pointer_checks() [1/2]

void goto_program_dereferencet::pointer_checks ( goto_programt goto_program)

Definition at line 366 of file goto_program_dereference.cpp.

References dereference_program(), and goto_program.

Referenced by pointer_checks().

◆ pointer_checks() [2/2]

void goto_program_dereferencet::pointer_checks ( goto_functionst goto_functions)

Definition at line 372 of file goto_program_dereference.cpp.

References dereference_program().

Member Data Documentation

◆ assertions

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

Definition at line 95 of file goto_program_dereference.h.

Referenced by dereference_failure(), and dereference_program().

◆ current_target

goto_programt::const_targett goto_program_dereferencet::current_target
protected

◆ dereference

value_set_dereferencet goto_program_dereferencet::dereference
protected

Definition at line 62 of file goto_program_dereference.h.

Referenced by dereference_rec().

◆ dereference_location

source_locationt goto_program_dereferencet::dereference_location
protected

Definition at line 92 of file goto_program_dereference.h.

Referenced by dereference_failure(), and dereference_rec().

◆ new_code

goto_programt goto_program_dereferencet::new_code
protected

Definition at line 96 of file goto_program_dereference.h.

Referenced by dereference_failure(), and dereference_program().

◆ ns

const namespacet& goto_program_dereferencet::ns
protected

◆ options

const optionst& goto_program_dereferencet::options
protected

Definition at line 59 of file goto_program_dereference.h.

Referenced by dereference_failure().

◆ value_sets

value_setst& goto_program_dereferencet::value_sets
protected

Definition at line 61 of file goto_program_dereference.h.

Referenced by get_value_set().


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