CBMC
instrumenter_pensievet Member List

This is the complete list of members for instrumenter_pensievet, including all inherited members.

add_instr_to_interleaving(goto_programt::instructionst::iterator it, goto_programt &interleaving)instrumentertinlineprotected
cfg_cycles_filter()instrumentert
collect_cycles(memory_modelt model)instrumentertinline
collect_cycles_by_SCCs(memory_modelt model)instrumentert
collect_pairs()instrumenter_pensievetinline
collect_pairs_naive()instrumenter_pensievetinline
cost(const event_grapht::critical_cyclet::delayt &e)instrumentertinlineprotected
egraphinstrumentert
egraph_altinstrumentertprotected
egraph_SCCsinstrumentert
extract_my_events()instrumentertstatic
goto2graph_cfg(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body)instrumentert
goto_functionsinstrumentertprotected
id2cyclocinstrumentert
id2locinstrumentert
instrument_all_inserter(const set_of_cyclest &set)instrumentertinlineprotected
instrument_minimum_interference_inserter(const set_of_cyclest &set)instrumentertinlineprotected
instrument_my_events(const std::set< event_idt > &events)instrumentert
instrument_my_events_inserter(const set_of_cyclest &set, const std::set< event_idt > &events)instrumentertinlineprotected
instrument_one_event_per_cycle_inserter(const set_of_cyclest &set)instrumentertinlineprotected
instrument_one_read_per_cycle_inserter(const set_of_cyclest &set)instrumentertinlineprotected
instrument_one_write_per_cycle_inserter(const set_of_cyclest &set)instrumentertinlineprotected
instrument_with_strategy(instrumentation_strategyt strategy)instrumentert
instrumenter_pensievet(goto_modelt &_goto_model, messaget &message)instrumenter_pensievetinline
instrumentert(goto_modelt &_goto_model, messaget &_message)instrumentertinline
is_cfg_spurious(const event_grapht::critical_cyclet &cyc)instrumentertprotected
local(const irep_idt &id)instrumentertinlineprotected
map_function_graphinstrumentert
map_function_nodest typedefinstrumentert
map_vertex_gnodeinstrumentertprotected
messageinstrumentert
nsinstrumentert
num_sccsinstrumentert
print_map_function_graph() constinstrumentertinline
print_outputs(memory_modelt model, bool hide_internals)instrumentert
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)instrumentertinlineprotected
render_by_fileinstrumentertprotected
render_by_functioninstrumentertprotected
render_po_alignedinstrumentertprotected
set_of_cyclesinstrumentert
set_of_cycles_per_SCCinstrumentert
set_of_cyclest typedefinstrumentertprotected
set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)instrumentertinline
set_rendering_options(bool aligned, bool file, bool function)instrumentertinline
target_sett typedefinstrumentertprotected
unique_idinstrumentertprotected
var_to_instrinstrumentert