cprover
Loading...
Searching...
No Matches
instrumenter_pensievet Class Reference

#include <instrumenter_pensieve.h>

Inheritance diagram for instrumenter_pensievet:
Collaboration diagram for instrumenter_pensievet:

Public Member Functions

 instrumenter_pensievet (goto_modelt &_goto_model, messaget &message)
void collect_pairs_naive ()
void collect_pairs ()
Public Member Functions inherited from instrumentert
void print_map_function_graph () const
 instrumentert (goto_modelt &_goto_model, messaget &_message)
unsigned goto2graph_cfg (value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body)
 goes through CFG and build a static abstract event graph overapproximating the read/write relations for any executions
void collect_cycles (memory_modelt model)
void collect_cycles_by_SCCs (memory_modelt model)
 Note: can be distributed (#define DISTRIBUTED)
void cfg_cycles_filter ()
void set_parameters_collection (unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
void instrument_with_strategy (instrumentation_strategyt strategy)
void instrument_my_events (const std::set< event_idt > &events)
void set_rendering_options (bool aligned, bool file, bool function)
void print_outputs (memory_modelt model, bool hide_internals)

Additional Inherited Members

Public Types inherited from instrumentert
typedef std::map< irep_idt, std::pair< std::set< event_idt >, std::set< event_idt > > > map_function_nodest
Static Public Member Functions inherited from instrumentert
static std::set< event_idtextract_my_events ()
Public Attributes inherited from instrumentert
namespacet ns
messagetmessage
event_grapht egraph
std::vector< std::set< event_idt > > egraph_SCCs
std::set< event_grapht::critical_cycletset_of_cycles
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
unsigned num_sccs
map_function_nodest map_function_graph
std::set< irep_idtvar_to_instr
std::multimap< irep_idt, source_locationtid2loc
std::multimap< irep_idt, source_locationtid2cycloc
Protected Types inherited from instrumentert
typedef std::set< event_grapht::critical_cycletset_of_cyclest
typedef std::set< goto_programt::instructiont::targetttarget_sett
Protected Member Functions inherited from instrumentert
bool local (const irep_idt &id)
 is local variable?
void add_instr_to_interleaving (goto_programt::instructionst::iterator it, goto_programt &interleaving)
bool is_cfg_spurious (const event_grapht::critical_cyclet &cyc)
unsigned cost (const event_grapht::critical_cyclet::delayt &e)
 cost function
void instrument_all_inserter (const set_of_cyclest &set)
void instrument_one_event_per_cycle_inserter (const set_of_cyclest &set)
void instrument_one_read_per_cycle_inserter (const set_of_cyclest &set)
void instrument_one_write_per_cycle_inserter (const set_of_cyclest &set)
void instrument_minimum_interference_inserter (const set_of_cyclest &set)
void instrument_my_events_inserter (const set_of_cyclest &set, const std::set< event_idt > &events)
void print_outputs_local (const std::set< event_grapht::critical_cyclet > &set, std::ofstream &dot, std::ofstream &ref, std::ofstream &output, std::ofstream &all, std::ofstream &table, memory_modelt model, bool hide_internals)
Protected Attributes inherited from instrumentert
goto_functionstgoto_functions
std::map< event_idt, event_idtmap_vertex_gnode
wmm_grapht egraph_alt
unsigned unique_id
bool render_po_aligned
bool render_by_file
bool render_by_function

Detailed Description

Definition at line 21 of file instrumenter_pensieve.h.

Constructor & Destructor Documentation

◆ instrumenter_pensievet()

instrumenter_pensievet::instrumenter_pensievet ( goto_modelt & _goto_model,
messaget & message )
inline

Definition at line 24 of file instrumenter_pensieve.h.

Member Function Documentation

◆ collect_pairs()

void instrumenter_pensievet::collect_pairs ( )
inline

Definition at line 35 of file instrumenter_pensieve.h.

◆ collect_pairs_naive()

void instrumenter_pensievet::collect_pairs_naive ( )
inline

Definition at line 29 of file instrumenter_pensieve.h.


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