#include <instrumenter_pensieve.h>

Inheritance diagram for instrumenter_pensievet:

Collaboration diagram for instrumenter_pensievet:

Public Member Functions
	instrumenter_pensievet (symbol_tablet &_symbol_table, goto_functionst &_goto_f, messaget &message)

void	collect_pairs_naive (namespacet &ns)

void	collect_pairs (namespacet &ns)

Public Member Functions inherited from instrumentert
void	print_map_function_graph () const

	instrumentert (symbol_tablet &_symbol_table, goto_functionst &_goto_f, 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