34{

35public:

40

42

44

49

54

59

61

62protected:

64};

67{

69

70 const symbol_table_baset::symbolst::const_iterator it =

72

74 return it->second;

75

76 w_guards.push_back(identifier);

77

80 new_symbol.base_name=identifier;

81 new_symbol.is_static_lifetime=true;

83

87}

90{

93

94 for(std::list<irep_idt>::const_iterator

97 it++)

98 {

99 exprt symbol=ns.lookup(*it).symbol_expr();

100

103

104 t++;

105 }

106}

109{

110 std::string result;

112 result="W/W";

113 else

114 result="R/W";

115

116 result+=" data race on ";

118 return result;

119}

122{

124

125 if(

127 identifier == CPROVER_PREFIX "alloc_size" || identifier == "stdin" ||

128 identifier == "stdout" || identifier == "stderr" ||

129 identifier == "sys_nerr" ||

130 identifier.starts_with("symex::invalid_object") ||

132 return false;

133

136}

139{

140 for(rw_set_baset::entriest::const_iterator

141 it=rw_set.r_entries.begin();

142 it!=rw_set.r_entries.end();

143 it++)

144 if(is_shared(ns, it->second.symbol_expr))

145 return true;

146

147 for(rw_set_baset::entriest::const_iterator

148 it=rw_set.w_entries.begin();

149 it!=rw_set.w_entries.end();

150 it++)

151 if(is_shared(ns, it->second.symbol_expr))

152 return true;

153

154 return false;

155}

168

169{

171

172#ifdef LOCAL_MAY

174#endif

175

177 {

179

181 {

183 ns,

184 value_sets,

185 function_id,

187 message_handler);

188

190 continue;

191

194

195 instruction =

198

199

201 {

203 continue;

204

205 goto_program.insert_before(

211 }

212

213

214 {

217 }

218

219

221 {

223 continue;

224

225 goto_program.insert_before(

231 }

232

233

235 {

237 continue;

238

242 goto_program.insert_before(

246 }

247

249 {

251 continue;

252

256 goto_program.insert_before(

260 }

261

262 i_it--;

263 }

264 }

265

267}

278{

279 w_guardst w_guards(symbol_table);

280

282 value_sets,

283 symbol_table,

284 function_id,

285 L_M_ARG(goto_function) goto_program,

286 w_guards,

287 message_handler);

288

290 goto_program.update();

291}

297{

299

301 {

302 if(

305 {

307 value_sets,

311 w_guards,

312 message_handler);

313 }

314 }

315

316

317 goto_functionst::function_mapt::iterator

320

322 throw "race check instrumentation needs an entry point";

323

327}

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

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.

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().

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.

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)

#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)