Go to the documentation of this file.
25 #define L_M_LAST_ARG(x) , x
28 #define L_M_LAST_ARG(x)
67 const symbol_tablet::symbolst::const_iterator it=
76 new_symbol.
name=identifier;
92 for(std::list<irep_idt>::const_iterator
115 result+=
" data race on ";
128 identifier==
"stdin" ||
129 identifier==
"stdout" ||
130 identifier==
"stderr" ||
131 identifier==
"sys_nerr" ||
144 for(rw_set_baset::entriest::const_iterator
148 if(
is_shared(ns, it->second.symbol_expr))
151 for(rw_set_baset::entriest::const_iterator
155 if(
is_shared(ns, it->second.symbol_expr))
186 original_instruction.
swap(instruction);
194 if(!
is_shared(ns, e_it->second.symbol_expr))
211 *t=original_instruction;
218 if(!
is_shared(ns, e_it->second.symbol_expr))
235 if(!
is_shared(ns, e_it->second.symbol_expr))
248 if(!
is_shared(ns, e_it->second.symbol_expr))
284 goto_program.update();
304 goto_functionst::function_mapt::iterator
309 throw "race check instrumentation needs an entry point";
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
source_locationt source_location
The location of the instruction in the source file.
#define forall_rw_set_w_entries(it, rw_set)
void set_comment(const irep_idt &comment)
std::string comment(const rw_set_baset::entryt &entry, bool write)
void swap(instructiont &instruction)
Swap two instructions.
typet type
Type of symbol.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
std::list< irep_idt > w_guards
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
function_mapt function_map
Expression to hold a symbol (variable)
const exprt get_assertion(const rw_set_baset::entryt &entry)
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().
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
const std::string & id2string(const irep_idt &d)
const symbolt & get_guard_symbol(const irep_idt &object)
bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
const irep_idt & get_identifier() const
#define forall_rw_set_r_entries(it, rw_set)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
#define INITIALIZE_FUNCTION
const exprt get_w_guard_expr(const rw_set_baset::entryt &entry)
The Boolean constant false.
symbol_tablet & symbol_table
#define Forall_goto_functions(it, functions)
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
::goto_functiont goto_functiont
instructionst instructions
The list of instructions in the goto program.
exprt value
Initial value of symbol.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
bool has_prefix(const std::string &s, const std::string &prefix)
void add_initialization(goto_programt &goto_program) const
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void race_check(value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, w_guardst &w_guards)
A codet representing an assignment in the program.
bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set)
This class represents an instruction in the GOTO intermediate representation.
symbol_tablet symbol_table
Symbol table.
irep_idt name
The unique identifier.
w_guardst(symbol_tablet &_symbol_table)
const exprt get_guard_symbol_expr(const irep_idt &object)
instructionst::iterator targett