32 unsigned unwinding_bound,
36 unsigned input_max_var,
37 unsigned input_max_po_trans,
62 message.status() <<
"Temporary variables added" <<
messaget::eom;
64 unsigned max_thds = 0;
65 instrumentert instrumenter(symbol_table, goto_functions, message);
67 no_dependencies, duplicate_body);
69 message.status() <<
"Abstract event graph computed" <<
messaget::eom;
72 if(input_max_var!=0 || input_max_po_trans!=0)
81 message.statistics() <<
"cycles collected: " <<
messaget::eom;
82 std::size_t interesting_scc = 0;
83 std::size_t total_cycles = 0;
84 for(std::size_t i=0; i<instrumenter.
num_sccs; i++)
87 message.statistics() <<
"SCC #" << i <<
": " 90 total_cycles += instrumenter
97 message.result() <<
"program safe -- no need to place additional fences" 110 message.statistics() <<
"cycles collected: " 118 <<
"program safe -- no need to place additional fences" 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 f...
instrumentation_strategyt
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
void print_map_function_graph() const
static mstreamt & eom(mstreamt &m)
void print_outputs(memory_modelt model, bool hide_internals)
void fence_weak_memory(memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, 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, bool print_graph, infer_modet mode, message_handlert &message_handler, bool ignore_arrays)
void collect_cycles(memory_modelt model)
void set_rendering_options(bool aligned, bool file, bool function)
ILP construction for cycles affecting user-assertions and resolution.
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
static irep_idt entry_point()
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
ILP construction for all cycles and resolution.
ILP construction for cycles containing user-placed fences and resolution.
#define Forall_goto_functions(it, functions)
std::set< event_grapht::critical_cyclet > set_of_cycles
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
std::vector< std::set< event_idt > > egraph_SCCs
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Race Detection for Threaded Goto Programs.