cprover
|
Weak Memory Instrumentation for Threaded Goto Programs. More...
#include "weak_memory.h"
#include <set>
#include <goto-programs/remove_skip.h>
#include <linking/static_lifetime_init.h>
#include <goto-instrument/rw_set.h>
#include "shared_buffers.h"
#include "goto2graph.h"
Go to the source code of this file.
Functions | |
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... | |
void | weak_memory (memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message_handler, bool ignore_arrays) |
Weak Memory Instrumentation for Threaded Goto Programs.
Definition in file weak_memory.cpp.
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 36 of file weak_memory.cpp.
References symbolt::base_name, goto_programt::instructiont::code, rw_set_baset::empty(), messaget::eom(), Forall_goto_program_instructions, goto_programt::instructiont::function, goto_program, goto_programt::instructiont::guard, id2string(), goto_programt::insert_before_swap(), goto_programt::instructiont::is_assert(), goto_programt::instructiont::is_assume(), goto_programt::instructiont::is_function_call(), goto_programt::instructiont::is_goto(), symbolt::is_static_lifetime, symbolt::is_thread_local, goto_programt::instructiont::make_assignment(), irept::make_nil(), symbol_tablet::move(), symbolt::name, goto_programt::instructiont::source_location, symbolt::symbol_expr(), to_string(), symbolt::type, and symbolt::value.
Referenced by weak_memory().
void weak_memory | ( | memory_modelt | model, |
value_setst & | value_sets, | ||
goto_modelt & | goto_model, | ||
bool | SCC, | ||
instrumentation_strategyt | event_strategy, | ||
unsigned | unwinding_bound, | ||
bool | no_cfg_kill, | ||
bool | no_dependencies, | ||
loop_strategyt | duplicate_body, | ||
unsigned | input_max_var, | ||
unsigned | input_max_po_trans, | ||
bool | render_po, | ||
bool | render_file, | ||
bool | render_function, | ||
bool | cav11_option, | ||
bool | hide_internals, | ||
message_handlert & | message_handler, | ||
bool | ignore_arrays | ||
) |
Definition at line 104 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(), shared_bufferst::cycles, shared_bufferst::cycles_loc, shared_bufferst::cycles_r_loc, instrumentert::egraph_SCCs, goto_functionst::entry_point(), messaget::eom(), instrumentert::extract_my_events(), Forall_goto_functions, instrumentert::goto2graph_cfg(), goto_modelt::goto_functions, instrumentert::id2cycloc, instrumentert::id2loc, id2string(), INITIALIZE_FUNCTION, instrumentert::instrument_my_events(), instrumentert::instrument_with_strategy(), introduce_temporaries(), message_handler, 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_modelt::symbol_table, goto_functionst::update(), instrumentert::var_to_instr, and shared_bufferst::cfg_visitort::weak_memory().
Referenced by goto_instrument_parse_optionst::instrument_goto_program().