cprover
instrumentert::cfg_visitort Class Reference

#include <goto2graph.h>

Collaboration diagram for instrumentert::cfg_visitort:
[legend]

Public Types

typedef std::multimap< irep_idt, event_idtid2nodet
 
typedef std::pair< irep_idt, event_idtid2node_pairt
 
typedef std::pair< event_idt, event_idtnodet
 
typedef std::map< goto_programt::const_targett, std::set< nodet > > incoming_post
 

Public Member Functions

virtual ~cfg_visitort ()
 
 cfg_visitort (namespacet &_ns, instrumentert &_instrumenter)
 
void enter_function (const irep_idt &function)
 
void leave_function (const irep_idt &function)
 
void visit_cfg (value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function)
 
virtual void visit_cfg_function (value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function, const std::set< nodet > &initial_vertex, std::set< nodet > &ending_vertex)
 TODO: move the visitor outside, and inherit. More...
 
bool local (const irep_idt &i)
 

Public Attributes

unsigned max_thread
 
id2nodet map_reads
 
id2nodet map_writes
 
unsigned write_counter
 
unsigned read_counter
 
unsigned ws_counter
 
unsigned fr_rf_counter
 
incoming_post in_pos
 
std::set< goto_programt::const_targettupdated
 
incoming_post out_pos
 
unsigned thread
 
data_dpt data_dp
 
std::set< event_idtunknown_read_nodes
 
std::set< event_idtunknown_write_nodes
 
std::set< irep_idtfunctions_met
 

Protected Member Functions

bool contains_shared_array (goto_programt::const_targett targ, goto_programt::const_targett i_it, value_setst &value_sets) const
 
void visit_cfg_thread () const
 
void visit_cfg_propagate (goto_programt::instructionst::iterator i_it)
 
void visit_cfg_body (goto_programt::const_targett i_it, loop_strategyt replicate_body, value_setst &value_sets)
 strategy: fwd/bwd alternation More...
 
void visit_cfg_backedge (goto_programt::const_targett targ, goto_programt::const_targett i_it)
 strategy: fwd/bwd alternation More...
 
void visit_cfg_duplicate (goto_programt::const_targett targ, goto_programt::const_targett i_it)
 
void visit_cfg_assign (value_setst &value_sets, namespacet &ns, goto_programt::instructionst::iterator &i_it, bool no_dependencies)
 
void visit_cfg_fence (goto_programt::instructionst::iterator i_it)
 
void visit_cfg_skip (goto_programt::instructionst::iterator i_it)
 
void visit_cfg_lwfence (goto_programt::instructionst::iterator i_it)
 
void visit_cfg_asm_fence (goto_programt::instructionst::iterator i_it)
 
void visit_cfg_function_call (value_setst &value_sets, goto_programt::instructionst::iterator i_it, memory_modelt model, bool no_dependenciess, loop_strategyt duplicate_body)
 
void visit_cfg_goto (goto_programt::instructionst::iterator i_it, loop_strategyt replicate_body, value_setst &value_sets)
 
void visit_cfg_reference_function (irep_idt id_function)
 references the first and last edges of the function More...
 

Protected Attributes

namespacetns
 
instrumentertinstrumenter
 
event_graphtegraph
 
std::vector< std::set< event_idt > > & egraph_SCCs
 
wmm_graphtegraph_alt
 
unsigned current_thread
 
unsigned coming_from
 

Detailed Description

Definition at line 89 of file goto2graph.h.

Member Typedef Documentation

◆ id2node_pairt

Definition at line 164 of file goto2graph.h.

◆ id2nodet

Definition at line 163 of file goto2graph.h.

◆ incoming_post

Definition at line 175 of file goto2graph.h.

◆ nodet

Definition at line 173 of file goto2graph.h.

Constructor & Destructor Documentation

◆ ~cfg_visitort()

virtual instrumentert::cfg_visitort::~cfg_visitort ( )
inlinevirtual

Definition at line 156 of file goto2graph.h.

◆ cfg_visitort()

instrumentert::cfg_visitort::cfg_visitort ( namespacet _ns,
instrumentert _instrumenter 
)
inline

Member Function Documentation

◆ contains_shared_array()

◆ enter_function()

void instrumentert::cfg_visitort::enter_function ( const irep_idt function)
inline

Definition at line 224 of file goto2graph.h.

References functions_met.

Referenced by visit_cfg().

◆ leave_function()

void instrumentert::cfg_visitort::leave_function ( const irep_idt function)
inline

Definition at line 231 of file goto2graph.h.

References functions_met.

Referenced by visit_cfg().

◆ local()

bool instrumentert::cfg_visitort::local ( const irep_idt i)
inline

Definition at line 80 of file goto2graph.cpp.

References instrumenter, and instrumentert::local().

◆ visit_cfg()

void instrumentert::cfg_visitort::visit_cfg ( value_setst value_sets,
memory_modelt  model,
bool  no_dependencies,
loop_strategyt  duplicate_body,
const irep_idt function 
)
inline

◆ visit_cfg_asm_fence()

◆ visit_cfg_assign()

◆ visit_cfg_backedge()

void instrumentert::cfg_visitort::visit_cfg_backedge ( goto_programt::const_targett  targ,
goto_programt::const_targett  i_it 
)
inlineprotected

◆ visit_cfg_body()

void instrumentert::cfg_visitort::visit_cfg_body ( goto_programt::const_targett  i_it,
loop_strategyt  replicate_body,
value_setst value_sets 
)
inlineprotected

strategy: fwd/bwd alternation

Definition at line 448 of file goto2graph.cpp.

References all_loops, arrays_only, and no_loop.

◆ visit_cfg_duplicate()

void instrumentert::cfg_visitort::visit_cfg_duplicate ( goto_programt::const_targett  targ,
goto_programt::const_targett  i_it 
)
inlineprotected

◆ visit_cfg_fence()

◆ visit_cfg_function()

void instrumentert::cfg_visitort::visit_cfg_function ( value_setst value_sets,
memory_modelt  model,
bool  no_dependencies,
loop_strategyt  duplicate_body,
const irep_idt function,
const std::set< nodet > &  initial_vertex,
std::set< nodet > &  ending_vertex 
)
virtual

◆ visit_cfg_function_call()

void instrumentert::cfg_visitort::visit_cfg_function_call ( value_setst value_sets,
goto_programt::instructionst::iterator  i_it,
memory_modelt  model,
bool  no_dependenciess,
loop_strategyt  duplicate_body 
)
protected

◆ visit_cfg_goto()

void instrumentert::cfg_visitort::visit_cfg_goto ( goto_programt::instructionst::iterator  i_it,
loop_strategyt  replicate_body,
value_setst value_sets 
)
protected

◆ visit_cfg_lwfence()

◆ visit_cfg_propagate()

void instrumentert::cfg_visitort::visit_cfg_propagate ( goto_programt::instructionst::iterator  i_it)
inlineprotected

◆ visit_cfg_reference_function()

void instrumentert::cfg_visitort::visit_cfg_reference_function ( irep_idt  id_function)
inlineprotected

references the first and last edges of the function

Definition at line 307 of file goto2graph.cpp.

References add_all_pos, messaget::debug(), messaget::eom(), id_function, and messaget::mstreamt::message.

◆ visit_cfg_skip()

void instrumentert::cfg_visitort::visit_cfg_skip ( goto_programt::instructionst::iterator  i_it)
protected

Definition at line 1143 of file goto2graph.cpp.

◆ visit_cfg_thread()

void instrumentert::cfg_visitort::visit_cfg_thread ( ) const
protected

Definition at line 297 of file goto2graph.cpp.

Member Data Documentation

◆ coming_from

unsigned instrumentert::cfg_visitort::coming_from
protected

Definition at line 102 of file goto2graph.h.

Referenced by cfg_visitort().

◆ current_thread

unsigned instrumentert::cfg_visitort::current_thread
protected

Definition at line 101 of file goto2graph.h.

Referenced by cfg_visitort().

◆ data_dp

data_dpt instrumentert::cfg_visitort::data_dp

Definition at line 200 of file goto2graph.h.

◆ egraph

event_grapht& instrumentert::cfg_visitort::egraph
protected

Definition at line 96 of file goto2graph.h.

◆ egraph_alt

wmm_grapht& instrumentert::cfg_visitort::egraph_alt
protected

Definition at line 98 of file goto2graph.h.

◆ egraph_SCCs

std::vector<std::set<event_idt> >& instrumentert::cfg_visitort::egraph_SCCs
protected

Definition at line 97 of file goto2graph.h.

◆ fr_rf_counter

unsigned instrumentert::cfg_visitort::fr_rf_counter

Definition at line 170 of file goto2graph.h.

Referenced by cfg_visitort(), and instrumentert::goto2graph_cfg().

◆ functions_met

std::set<irep_idt> instrumentert::cfg_visitort::functions_met

Definition at line 207 of file goto2graph.h.

Referenced by enter_function(), and leave_function().

◆ in_pos

incoming_post instrumentert::cfg_visitort::in_pos

Definition at line 177 of file goto2graph.h.

◆ instrumenter

instrumentert& instrumentert::cfg_visitort::instrumenter
protected

Definition at line 93 of file goto2graph.h.

Referenced by local(), and visit_cfg().

◆ map_reads

id2nodet instrumentert::cfg_visitort::map_reads

Definition at line 165 of file goto2graph.h.

◆ map_writes

id2nodet instrumentert::cfg_visitort::map_writes

Definition at line 165 of file goto2graph.h.

◆ max_thread

unsigned instrumentert::cfg_visitort::max_thread

Definition at line 160 of file goto2graph.h.

Referenced by cfg_visitort(), and instrumentert::goto2graph_cfg().

◆ ns

namespacet& instrumentert::cfg_visitort::ns
protected

Definition at line 92 of file goto2graph.h.

◆ out_pos

incoming_post instrumentert::cfg_visitort::out_pos

Definition at line 181 of file goto2graph.h.

◆ read_counter

unsigned instrumentert::cfg_visitort::read_counter

Definition at line 168 of file goto2graph.h.

Referenced by cfg_visitort(), and instrumentert::goto2graph_cfg().

◆ thread

unsigned instrumentert::cfg_visitort::thread

Definition at line 197 of file goto2graph.h.

Referenced by cfg_visitort().

◆ unknown_read_nodes

std::set<event_idt> instrumentert::cfg_visitort::unknown_read_nodes

Definition at line 203 of file goto2graph.h.

◆ unknown_write_nodes

std::set<event_idt> instrumentert::cfg_visitort::unknown_write_nodes

Definition at line 204 of file goto2graph.h.

◆ updated

std::set<goto_programt::const_targett> instrumentert::cfg_visitort::updated

Definition at line 178 of file goto2graph.h.

◆ write_counter

unsigned instrumentert::cfg_visitort::write_counter

Definition at line 167 of file goto2graph.h.

Referenced by cfg_visitort(), and instrumentert::goto2graph_cfg().

◆ ws_counter

unsigned instrumentert::cfg_visitort::ws_counter

Definition at line 169 of file goto2graph.h.

Referenced by cfg_visitort(), and instrumentert::goto2graph_cfg().


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