CBMC
Public Member Functions | List of all members
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 More...
 
void collect_cycles (memory_modelt model)
 
void collect_cycles_by_SCCs (memory_modelt model)
 Note: can be distributed (#define DISTRIBUTED) More...
 
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_idt > extract_my_events ()
 
- Public Attributes inherited from instrumentert
namespacet ns
 
messaget & message
 
event_grapht egraph
 
std::vector< std::set< event_idt > > egraph_SCCs
 
std::set< event_grapht::critical_cyclet > set_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_idt > var_to_instr
 
std::multimap< irep_idt, source_locationt > id2loc
 
std::multimap< irep_idt, source_locationt > id2cycloc
 
- Protected Types inherited from instrumentert
typedef std::set< event_grapht::critical_cyclet > set_of_cyclest
 
typedef std::set< goto_programt::instructiont::targett > target_sett
 
- Protected Member Functions inherited from instrumentert
bool local (const irep_idt &id)
 is local variable? More...
 
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 More...
 
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_functionst & goto_functions
 
std::map< event_idt, event_idt > map_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: