33 #define L_M_LAST_ARG(x) , x 36 #define L_M_LAST_ARG(x) 75 const symbol_tablet::symbolst::const_iterator it=
84 new_symbol.
name=identifier;
100 for(std::list<irep_idt>::const_iterator
123 result+=
" data race on ";
136 identifier==
"stdin" ||
137 identifier==
"stdout" ||
138 identifier==
"stderr" ||
139 identifier==
"sys_nerr" ||
152 for(rw_set_baset::entriest::const_iterator
156 if(
is_shared(ns, it->second.symbol_expr))
159 for(rw_set_baset::entriest::const_iterator
163 if(
is_shared(ns, it->second.symbol_expr))
184 goto_programt::instructiont &instruction=*i_it;
186 if(instruction.is_assign())
193 goto_programt::instructiont original_instruction;
194 original_instruction.swap(instruction);
196 instruction.make_skip();
202 if(!
is_shared(ns, e_it->second.symbol_expr))
219 *t=original_instruction;
226 if(!
is_shared(ns, e_it->second.symbol_expr))
243 if(!
is_shared(ns, e_it->second.symbol_expr))
249 t->source_location=original_instruction.source_location;
250 t->source_location.set_comment(
comment(e_it->second,
false));
256 if(!
is_shared(ns, e_it->second.symbol_expr))
262 t->source_location=original_instruction.source_location;
263 t->source_location.set_comment(
comment(e_it->second,
true));
292 goto_program.update();
313 goto_functionst::function_mapt::iterator
317 throw "race check instrumentation needs an entry point";
irep_idt name
The unique identifier.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
std::string comment(const rw_set_baset::entryt &entry, bool write)
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
Goto Programs with Functions.
#define forall_rw_set_w_entries(it, rw_set)
exprt value
Initial value of symbol.
const exprt get_guard_symbol_expr(const irep_idt &object)
Race Detection for Threaded Goto Programs.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
#define forall_rw_set_r_entries(it, rw_set)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
static irep_idt entry_point()
API to expression classes.
void add_initialization(goto_programt &goto_program) const
bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
goto_function_templatet< goto_programt > goto_functiont
function_mapt function_map
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
The boolean constant false.
bool has_prefix(const std::string &s, const std::string &prefix)
targett insert_before(const_targett target)
Insertion before the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
w_guardst(symbol_tablet &_symbol_table)
Base class for all expressions.
const symbolt & get_guard_symbol(const irep_idt &object)
irep_idt base_name
Base (non-scoped) name.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
const exprt get_w_guard_expr(const rw_set_baset::entryt &entry)
void race_check(value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, w_guardst &w_guards)
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
std::list< irep_idt > w_guards
symbol_tablet & symbol_table
bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
const exprt get_assertion(const rw_set_baset::entryt &entry)
Field-insensitive, location-sensitive may-alias analysis.
instructionst::iterator targett
Race Detection for Threaded Goto Programs.