27 #define L_M_LAST_ARG(x) , x
30 #define L_M_LAST_ARG(x)
70 const symbol_table_baset::symbolst::const_iterator it =
80 new_symbol.base_name=identifier;
81 new_symbol.is_static_lifetime=
true;
94 for(std::list<irep_idt>::const_iterator
116 result+=
" data race on ";
127 identifier ==
CPROVER_PREFIX "alloc_size" || identifier ==
"stdin" ||
128 identifier ==
"stdout" || identifier ==
"stderr" ||
129 identifier ==
"sys_nerr" ||
140 for(rw_set_baset::entriest::const_iterator
144 if(
is_shared(ns, it->second.symbol_expr))
147 for(rw_set_baset::entriest::const_iterator
151 if(
is_shared(ns, it->second.symbol_expr))
193 original_instruction.
swap(instruction);
200 for(
const auto &w_entry : rw_set.
w_entries)
202 if(!
is_shared(ns, w_entry.second.symbol_expr))
205 goto_program.insert_before(
209 w_entry.second.guard,
216 *t=original_instruction;
220 for(
const auto &w_entry : rw_set.
w_entries)
222 if(!
is_shared(ns, w_entry.second.symbol_expr))
225 goto_program.insert_before(
234 for(
const auto &r_entry : rw_set.
r_entries)
236 if(!
is_shared(ns, r_entry.second.symbol_expr))
242 goto_program.insert_before(
245 w_guards.
get_assertion(r_entry.second), annotated_location));
248 for(
const auto &w_entry : rw_set.
w_entries)
250 if(!
is_shared(ns, w_entry.second.symbol_expr))
256 goto_program.insert_before(
259 w_guards.
get_assertion(w_entry.second), annotated_location));
285 L_M_ARG(goto_function) goto_program,
290 goto_program.update();
310 L_M_ARG(gf_entry.second) gf_entry.second.body,
317 goto_functionst::function_mapt::iterator
322 throw "race check instrumentation needs an entry point";
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Base class for all expressions.
The Boolean constant false.
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
const source_locationt & source_location() const
void swap(instructiont &instruction)
Swap two instructions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void set_comment(const irep_idt &comment)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The symbol table base class interface.
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
irep_idt mode
Language mode.
std::list< irep_idt > w_guards
const symbolt & get_guard_symbol(const irep_idt &object)
const exprt get_assertion(const rw_set_baset::entryt &entry)
void add_initialization(goto_programt &goto_program) const
const exprt get_w_guard_expr(const rw_set_baset::entryt &entry)
symbol_table_baset & symbol_table
const exprt get_guard_symbol_expr(const irep_idt &object)
w_guardst(symbol_table_baset &_symbol_table)
int main(int argc, char *argv[])
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Field-insensitive, location-sensitive may-alias analysis.
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
static void race_check(value_setst &value_sets, symbol_table_baset &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards, message_handlert &message_handler)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
Race Detection for Threaded Goto Programs.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Race Detection for Threaded Goto Programs.
#define INITIALIZE_FUNCTION
ssize_t write(int fildes, const void *buf, size_t nbyte)