cprover
|
Weak Memory Instrumentation for Threaded Goto Programs. More...
Go to the source code of this file.
Functions | |
void | weak_memory (memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, bool SCC, instrumentation_strategyt event_stategy, unsigned unwinding_bound, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned max_var, unsigned max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message, bool ignore_arrays) |
void | introduce_temporaries (value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function, goto_programt &goto_program, messaget &message) |
all access to shared variables is pushed into assignments More... | |
Weak Memory Instrumentation for Threaded Goto Programs.
Definition in file weak_memory.h.
void introduce_temporaries | ( | value_setst & | value_sets, |
symbol_tablet & | symbol_table, | ||
const irep_idt & | function, | ||
goto_programt & | goto_program, | ||
messaget & | message | ||
) |
all access to shared variables is pushed into assignments
Definition at line 38 of file weak_memory.cpp.
References symbolt::base_name, rw_set_baset::empty(), messaget::eom(), Forall_goto_program_instructions, id2string(), goto_program_templatet< codeT, guardT >::insert_before_swap(), symbolt::is_static_lifetime, symbolt::is_thread_local, irept::make_nil(), symbol_tablet::move(), symbolt::name, symbolt::symbol_expr(), symbolt::type, and symbolt::value.
Referenced by fence_pensieve(), fence_weak_memory(), and weak_memory().
void weak_memory | ( | memory_modelt | model, |
value_setst & | value_sets, | ||
symbol_tablet & | symbol_table, | ||
goto_functionst & | goto_functions, | ||
bool | SCC, | ||
instrumentation_strategyt | event_stategy, | ||
unsigned | unwinding_bound, | ||
bool | no_cfg_kill, | ||
bool | no_dependencies, | ||
loop_strategyt | duplicate_body, | ||
unsigned | max_var, | ||
unsigned | max_po_trans, | ||
bool | render_po, | ||
bool | render_file, | ||
bool | render_function, | ||
bool | cav11_option, | ||
bool | hide_internals, | ||
message_handlert & | message, | ||
bool | ignore_arrays | ||
) |
Definition at line 106 of file weak_memory.cpp.
References shared_bufferst::add_initialization_code(), shared_bufferst::affected_by_delay(), shared_bufferst::affected_by_delay_set, instrumentert::cfg_cycles_filter(), instrumentert::collect_cycles(), instrumentert::collect_cycles_by_SCCs(), CPROVER_PREFIX, shared_bufferst::cycles, shared_bufferst::cycles_loc, shared_bufferst::cycles_r_loc, instrumentert::egraph_SCCs, goto_functions_templatet< goto_programt >::entry_point(), goto_functions_templatet< bodyT >::entry_point(), messaget::eom(), instrumentert::extract_my_events(), Forall_goto_functions, instrumentert::goto2graph_cfg(), instrumentert::id2cycloc, instrumentert::id2loc, id2string(), instrumentert::instrument_my_events(), instrumentert::instrument_with_strategy(), introduce_temporaries(), my_events, instrumentert::num_sccs, instrumentert::print_outputs(), remove_skip(), shared_bufferst::set_cav11(), instrumentert::set_of_cycles, instrumentert::set_of_cycles_per_SCC, instrumentert::set_parameters_collection(), instrumentert::set_rendering_options(), messaget::status(), goto_functions_templatet< bodyT >::update(), instrumentert::var_to_instr, and shared_bufferst::cfg_visitort::weak_memory().
Referenced by goto_instrument_parse_optionst::instrument_goto_program().