23 unsigned unwinding_bound,
24 unsigned input_max_po_trans,
45 message.status() <<
"Temporary variables added" <<
messaget::eom;
47 unsigned max_thds = 0;
51 message.status() <<
"Abstract event graph computed" <<
messaget::eom;
53 if(input_max_po_trans!=0)
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...
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
static mstreamt & eom(mstreamt &m)
Fence insertion following criteria of Pensieve (PPoPP'05)
static irep_idt entry_point()
void collect_pairs_naive(namespacet &ns)
void fence_pensieve(value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, unsigned unwinding_bound, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool naive_mode, message_handlert &message_handler)
void collect_pairs(namespacet &ns)
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
#define Forall_goto_functions(it, functions)
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
Race Detection for Threaded Goto Programs.