47 identifier==
"stdin" ||
48 identifier==
"stdout" ||
49 identifier==
"stderr" ||
50 identifier==
"sys_nerr" ||
54 const size_t pos=identifier.find(
"[]");
56 if(
pos!=std::string::npos)
59 identifier.erase(
pos);
64 const symbolt &symbol=
ns.lookup(identifier);
74 catch(
const std::string &exception)
99 visitor.
visit_cfg(value_sets, model, no_dependencies, duplicate_body,
102 std::vector<std::size_t> subgraph_index;
106 for(std::map<event_idt, event_idt>::const_iterator
111 const std::size_t sg=subgraph_index[it->second];
115 message.status() <<
"Number of threads detected: "
119 unsigned interesting_sccs=0;
125 << interesting_sccs <<
" interesting SCCs"
136 std::size_t instr_counter=0;
137 for(goto_functionst::function_mapt::const_iterator
141 instr_counter+=it->second.body.instructions.size();
142 message.statistics() <<
"Number of goto-instructions: "
151 bool no_dependencies,
154 std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)
173 instrumenter.goto_functions.function_map[function_id].body;
202 #elif defined ATOMIC_FENCE
245 no_dependencies, replicate_body);
261#ifdef CONTEXT_INSENSITIVE
276 egraph.map_data_dp.insert(new_dp);
279 if(
instrumenter.goto_functions.function_map[function_id]
280 .body.instructions.empty())
286 goto_programt::instructionst::iterator it =
288 .body.instructions.end();
295 goto_programt::instructionst::iterator i_it)
302 for(
const auto &node :
in_pos[in])
303 in_pos[i_it].insert(node);
334 goto_programt::instructionst::iterator i_it=body.end();
338 goto_programt::instructionst::iterator targ=body.begin();
340 std::set<event_idt> in_nodes;
341 std::set<event_idt> out_nodes;
350 for(std::set<nodet>::const_iterator to=
in_pos[targ].begin();
351 to!=
in_pos[targ].end(); ++to)
352 in_nodes.insert(to->first);
353 for(std::set<nodet>::const_iterator from=
in_pos[i_it].begin();
354 from!=
in_pos[i_it].end(); ++from)
355 out_nodes.insert(from->first);
361 for(goto_programt::instructionst::iterator cur=i_it;
365 for(
const auto &in : cur->incoming_edges)
385 for(std::set<nodet>::const_iterator to=
out_pos[targ].begin();
387 in_nodes.insert(to->first);
388 for(std::set<nodet>::const_iterator from=
in_pos[i_it].begin();
389 from!=
in_pos[i_it].end(); ++from)
390 out_nodes.insert(from->first);
396 std::make_pair(in_nodes, out_nodes);
420 <<
"contains_shared_array called for " << targ->source_location().get_line()
421 <<
" and " << i_it->source_location().get_line() <<
messaget::eom;
425 <<
"Do we have an array at line " << cur->source_location().get_line()
439 for(
const auto &r_entry : rw_set.
r_entries)
441 const irep_idt var = r_entry.second.object;
442 instrumenter.message.debug() <<
"Is "<<var<<
" an array?"
444 if(
id2string(var).find(
"[]")!=std::string::npos
449 for(
const auto &w_entry : rw_set.
w_entries)
451 const irep_idt var = w_entry.second.object;
453 if(
id2string(var).find(
"[]")!=std::string::npos
477 for(
const auto &target : i_it->targets)
485 bool duplicate_this=
false;
487 switch(replicate_body)
505 duplicate_this=
false;
524 bool found_pos=
false;
530 for(; new_targ != goto_program.
instructions.end(); ++new_targ)
544 new_targ->source_location().get_function() !=
545 targ->source_location().get_function() ||
546 new_targ->source_location().get_file() !=
547 targ->source_location().get_file())
552 const std::set<nodet> &up_set=
in_pos[(found_pos ? new_targ : targ)];
553 const std::set<nodet> &down_set=
in_pos[i_it];
555 for(std::set<nodet>::const_iterator begin_it=up_set.begin();
556 begin_it!=up_set.end(); ++begin_it)
559 for(std::set<nodet>::const_iterator begin_it=down_set.begin();
560 begin_it!=down_set.end(); ++begin_it)
563 for(std::set<nodet>::const_iterator begin_it=up_set.begin();
564 begin_it!=up_set.end(); ++begin_it)
566 for(std::set<nodet>::const_iterator end_it=down_set.begin();
567 end_it!=down_set.end(); ++end_it)
569 egraph.copy_segment(begin_it->first, end_it->first);
572 const event_idt end=
egraph.copy_segment(begin_it->first, end_it->first);
591 for(std::set<nodet>::const_iterator to=
in_pos[targ].begin();
592 to!=
in_pos[targ].end(); ++to)
593 for(std::set<nodet>::const_iterator from=
in_pos[i_it].begin();
594 from!=
in_pos[i_it].end(); ++from)
595 if(from->first!=to->first)
597 if(
egraph[from->first].thread!=
egraph[to->first].thread)
601 egraph.add_po_back_edge(from->first, to->first);
602 egraph_alt.add_edge(from->second, to->second);
613 for(
const auto &in : cur->incoming_edges)
632 for(std::set<nodet>::const_iterator to=
out_pos[targ].begin();
634 for(std::set<nodet>::const_iterator from=
in_pos[i_it].begin();
635 from!=
in_pos[i_it].end(); ++from)
636 if(from->first!=to->first)
638 if(
egraph[from->first].thread!=
egraph[to->first].thread)
642 egraph.add_po_back_edge(from->first, to->first);
643 egraph_alt.add_edge(from->second, to->second);
652 goto_programt::instructionst::iterator i_it,
689 goto_programt::instructionst::iterator i_it,
691 bool no_dependencies,
702 #ifdef CONTEXT_INSENSITIVE
703 stack_fun.push(cur_fun);
708 if(!inline_function_cond(fun_id))
737 #ifdef CONTEXT_INSENSITIVE
738 cur_fun=stack_fun.pop();
741 catch(
const std::string &s)
743 instrumenter.message.warning() <<
"sorry, doesn't handle recursion "
744 <<
"(function " << fun_id <<
"; .cpp) "
750 goto_programt::instructionst::iterator i_it,
763 egraph[new_fence_node](new_fence_event);
767 std::make_pair(new_fence_node, new_fence_gnode));
772 for(
const auto &node :
in_pos[in])
776 instrumenter.message.debug() << node.first<<
"-po->"<<new_fence_node
778 egraph.add_po_edge(node.first, new_fence_node);
779 egraph_alt.add_edge(node.second, new_fence_gnode);
784 in_pos[i_it].insert(
nodet(new_fence_node, new_fence_gnode));
789 goto_programt::instructionst::iterator i_it,
816 egraph[new_fence_node](new_fence_event);
820 std::make_pair(new_fence_node, new_fence_gnode));
825 for(
const auto &node :
in_pos[in])
829 instrumenter.message.debug() << node.first<<
"-po->"<<new_fence_node
831 egraph.add_po_edge(node.first, new_fence_node);
832 egraph_alt.add_edge(node.second, new_fence_gnode);
837 in_pos[i_it].insert(
nodet(new_fence_node, new_fence_gnode));
844 goto_programt::instructionst::iterator &i_it,
865 event_idt previous=std::numeric_limits<event_idt>::max();
866 event_idt previous_gnode=std::numeric_limits<event_idt>::max();
873 if(!instruction.
labels.empty() && instruction.
labels.front()==
"ASSERT")
877 for(
const auto &r_entry : rw_set.
r_entries)
883 const irep_idt &read = r_entry.second.object;
904 egraph[new_read_node]=new_read_event;
907 << (
local(read) ?
"local" :
"shared") <<
") #"
916 std::make_pair(new_read_node, new_read_gnode));
923 for(
const auto &node :
in_pos[in])
929 egraph.add_po_edge(node.first, new_read_node);
930 egraph_alt.add_edge(node.second, new_read_gnode);
936 previous=new_read_node;
937 previous_gnode=new_read_gnode;
940 const std::pair<id2nodet::iterator, id2nodet::iterator>
942 for(id2nodet::iterator id_it=with_same_var.first;
943 id_it!=with_same_var.second; id_it++)
946 instrumenter.message.debug() << id_it->second<<
"<-com->"
948 std::map<event_idt, event_idt>::const_iterator entry=
951 egraph.add_com_edge(new_read_node, id_it->second);
952 egraph_alt.add_edge(new_read_gnode, entry->second);
953 egraph.add_com_edge(id_it->second, new_read_node);
954 egraph_alt.add_edge(entry->second, new_read_gnode);
959 for(std::set<event_idt>::const_iterator id_it=
967 std::map<event_idt, event_idt>::const_iterator entry=
970 egraph.add_com_edge(new_read_node, *id_it);
971 egraph_alt.add_edge(new_read_gnode, entry->second);
972 egraph.add_com_edge(*id_it, new_read_node);
973 egraph_alt.add_edge(entry->second, new_read_gnode);
979 for(
const auto &w_entry : rw_set.
w_entries)
985 const irep_idt &write = w_entry.second.object;
1007 egraph[new_write_node](new_write_event);
1009 <<
"new Write " << write <<
" @thread" << (
thread) <<
"("
1011 << (
local(write) ?
"local" :
"shared") <<
") #" << new_write_node
1014 if(write==ID_unknown)
1020 std::pair<event_idt, event_idt>(new_write_node, new_write_gnode));
1023 if(previous!=std::numeric_limits<event_idt>::max())
1025 instrumenter.message.debug() << previous<<
"-po->"<<new_write_node
1027 egraph.add_po_edge(previous, new_write_node);
1028 egraph_alt.add_edge(previous_gnode, new_write_gnode);
1036 for(
const auto &node :
in_pos[in])
1042 egraph.add_po_edge(node.first, new_write_node);
1043 egraph_alt.add_edge(node.second, new_write_gnode);
1050 const std::pair<id2nodet::iterator, id2nodet::iterator>
1051 r_with_same_var=
map_reads.equal_range(write);
1052 for(id2nodet::iterator idr_it=r_with_same_var.first;
1053 idr_it!=r_with_same_var.second; idr_it++)
1054 if(
egraph[idr_it->second].thread!=new_write_event.
thread)
1056 instrumenter.message.debug() <<idr_it->second<<
"<-com->"
1058 std::map<event_idt, event_idt>::const_iterator entry=
1061 egraph.add_com_edge(new_write_node, idr_it->second);
1062 egraph_alt.add_edge(new_write_gnode, entry->second);
1063 egraph.add_com_edge(idr_it->second, new_write_node);
1064 egraph_alt.add_edge(entry->second, new_write_gnode);
1069 const std::pair<id2nodet::iterator, id2nodet::iterator>
1070 w_with_same_var=
map_writes.equal_range(write);
1071 for(id2nodet::iterator idw_it=w_with_same_var.first;
1072 idw_it!=w_with_same_var.second; idw_it++)
1073 if(
egraph[idw_it->second].thread!=new_write_event.
thread)
1075 instrumenter.message.debug() << idw_it->second<<
"<-com->"
1077 std::map<event_idt, event_idt>::const_iterator entry=
1080 egraph.add_com_edge(new_write_node, idw_it->second);
1081 egraph_alt.add_edge(new_write_gnode, entry->second);
1082 egraph.add_com_edge(idw_it->second, new_write_node);
1083 egraph_alt.add_edge(entry->second, new_write_gnode);
1088 for(std::set<event_idt>::const_iterator id_it=
1096 std::map<event_idt, event_idt>::const_iterator entry=
1099 egraph.add_com_edge(new_write_node, *id_it);
1100 egraph_alt.add_edge(new_write_gnode, entry->second);
1101 egraph.add_com_edge(*id_it, new_write_node);
1102 egraph_alt.add_edge(entry->second, new_write_gnode);
1107 for(std::set<event_idt>::const_iterator id_it=
1115 std::map<event_idt, event_idt>::const_iterator entry=
1118 egraph.add_com_edge(new_write_node, *id_it);
1119 egraph_alt.add_edge(new_write_gnode, entry->second);
1120 egraph.add_com_edge(*id_it, new_write_node);
1121 egraph_alt.add_edge(entry->second, new_write_gnode);
1127 previous=new_write_node;
1128 previous_gnode=new_write_gnode;
1131 if(previous!=std::numeric_limits<event_idt>::max())
1134 in_pos[i_it].insert(
nodet(previous, previous_gnode));
1144 if(!no_dependencies)
1146 for(
const auto &w_entry : rw_set.
w_entries)
1148 for(
const auto &r_entry : rw_set.
r_entries)
1150 const irep_idt &write = w_entry.second.object;
1151 const irep_idt &read = r_entry.second.object;
1152 instrumenter.message.debug() <<
"dp: Write:"<<write<<
"; Read:"<<read
1161 for(
const auto &r_entry : rw_set.
r_entries)
1163 for(
const auto &r_entry2 : rw_set.
r_entries)
1165 const irep_idt &read2 = r_entry2.second.object;
1166 const irep_idt &read = r_entry.second.object;
1179 goto_programt::instructionst::iterator i_it,
1192 egraph[new_fence_node](new_fence_event);
1196 std::make_pair(new_fence_node, new_fence_gnode));
1201 for(
const auto &node :
in_pos[in])
1203 instrumenter.message.debug() << node.first<<
"-po->"<<new_fence_node
1205 egraph.add_po_edge(node.first, new_fence_node);
1206 egraph_alt.add_edge(node.second, new_fence_gnode);
1211 s.insert(
nodet(new_fence_node, new_fence_gnode));
1216 in_pos[i_it].insert(
nodet(new_fence_node, new_fence_gnode));
1221 goto_programt::instructionst::iterator i_it)
1227 goto_programt::instructionst::iterator it,
1231 it->is_set_return_value() || it->is_throw() || it->is_catch() ||
1232 it->is_skip() || it->is_dead() || it->is_start_thread() ||
1233 it->is_end_thread())
1236 if(it->is_atomic_begin() ||
1237 it->is_atomic_end())
1243 if(it->is_function_call())
1259 e_it!=cyc.
end() && ++e_it!=cyc.
end(); ++e_it)
1268 bool thread_found=
false;
1272 for(
const auto &instruction : gf_entry.second.body.instructions)
1274 if(instruction.source_location() == current_location)
1276 current_po = &gf_entry.second.body;
1291 bool exists_n=
false;
1293 for(wmm_grapht::edgest::const_iterator edge_it=pos_cur.begin();
1294 edge_it!=pos_cur.end(); edge_it++)
1296 if(pos_next.find(edge_it->first)!=pos_next.end())
1304 if((++e_it)!=cyc.
end() || !exists_n)
1310 if(i_it->source_location() == current_location)
1313 for(goto_programt::instructionst::iterator same_loc = i_it;
1315 same_loc->source_location() == i_it->source_location();
1329 bool in_cycle=
false;
1332 if(it->source_location() == current_location)
1337 if(it->source_location() == next_location)
1350 if(instruction.is_goto())
1352 for(
const auto &t : instruction.targets)
1354 bool target_in_cycle=
false;
1360 target_in_cycle=
true;
1365 if(!target_in_cycle)
1379 map.insert(std::make_pair(
1381 std::move(one_interleaving)));
1388 bmct bmc(no_option, symbol_table, no_message);
1390 bool is_spurious=bmc.run(this_interleaving);
1404 for(std::set<event_grapht::critical_cyclet>::iterator
1410 std::set<event_grapht::critical_cyclet>::iterator next=it;
1425 for(std::set<event_grapht::critical_cyclet>::iterator it=
1431 std::set<event_grapht::critical_cyclet>::iterator next=it;
1448 const std::set<event_grapht::critical_cyclet> &set,
1451 std::ofstream &output,
1453 std::ofstream &table,
1455 bool hide_internals)
1458 std::map<unsigned, std::set<event_idt> > same_po;
1459 unsigned max_thread=0;
1463 std::map<irep_idt, std::set<event_idt> > same_file;
1466 std::map<std::string, std::string> map_id2var;
1467 std::map<std::string, std::string> map_var2id;
1469 for(std::set<event_grapht::critical_cyclet>::const_iterator it =
1470 set.begin(); it!=set.end(); it++)
1475 it->print_dot(
dot, colour++, model);
1476 ref << it->print_name(model, hide_internals) <<
'\n';
1477 output << it->print_output() <<
'\n';
1478 all << it->print_all(model, map_id2var, map_var2id, hide_internals)
1482 for(std::list<event_idt>::const_iterator it_e=it->begin();
1483 it_e!=it->end(); it_e++)
1488 same_po[ev.
thread].insert(*it_e);
1499 dot << ev.
id <<
"[label=\"\\\\lb {" << ev.
id <<
"}";
1501 dot << ev.
thread <<
"\",color=red,shape=box];\n";
1509 for(
unsigned i=0; i<=max_thread; i++)
1510 if(!same_po[i].empty())
1512 dot <<
"{rank=same; thread_" << i
1513 <<
"[shape=plaintext, label=\"thread " << i <<
"\"];";
1514 for(std::set<event_idt>::iterator it=same_po[i].begin();
1515 it!=same_po[i].end(); it++)
1524 for(std::map<
irep_idt, std::set<event_idt> >::const_iterator it=
1526 it!=same_file.end(); it++)
1529 dot <<
" label=\"" << it->first <<
"\";\n";
1530 for(std::set<event_idt>::const_iterator ev_it=it->second.begin();
1531 ev_it!=it->second.end(); ev_it++)
1533 dot <<
" " <<
egraph[*ev_it].id <<
";\n";
1540 table << std::string(80,
'-');
1541 for(std::map<std::string, std::string>::const_iterator
1542 m_it=map_id2var.begin();
1543 m_it!=map_id2var.end();
1546 table <<
"\n| " << m_it->first <<
" : " << m_it->second;
1549 table << std::string(80,
'-');
1557 std::ofstream output;
1559 std::ofstream table;
1561 dot.open(
"cycles.dot");
1562 ref.open(
"ref.txt");
1563 output.open(
"output.txt");
1564 all.open(
"all.txt");
1565 table.open(
"table.txt");
1567 dot <<
"digraph G {\n";
1568 dot <<
"nodesep=1; ranksep=1;\n";
1573 model, hide_internals);
1578 std::ofstream local_dot;
1579 std::string name=
"scc_" + std::to_string(i) +
".dot";
1580 local_dot.open(name.c_str());
1582 local_dot <<
"digraph G {\n";
1583 local_dot <<
"nodesep=1; ranksep=1;\n";
1585 table, model, hide_internals);
1589 dot << i <<
"[label=\"SCC " << i <<
"\",link=\"" <<
"scc_" << i;
1612 std::set<event_grapht::critical_cyclet>());
1613 for(std::vector<std::set<event_idt> >::const_iterator it=
egraph_SCCs.begin();
1619class pthread_argumentt
1624 const std::set<event_idt> &filter;
1625 std::set<event_grapht::critical_cyclet> &cycles;
1629 const std::set<event_idt> &_filter,
1630 std::set<event_grapht::critical_cyclet> &_cycles)
1631 :instr(_instr), mem(_mem), filter(_filter), cycles(_cycles)
1637void *collect_cycles_in_thread(
void *arg)
1640 pthread_argumentt *p_arg=
reinterpret_cast<pthread_argumentt*
>(arg);
1643 const std::set<event_idt> &filter=p_arg->filter;
1644 std::set<event_grapht::critical_cyclet> &cycles=p_arg->cycles;
1653 const unsigned number_of_sccs=
num_sccs;
1654 std::set<unsigned> interesting_SCCs;
1657 pthread_t *threads=
new pthread_t[
num_sccs+1];
1660 std::set<event_grapht::critical_cyclet>());
1662 for(std::vector<std::set<unsigned> >::const_iterator it=
egraph_SCCs.begin();
1666 interesting_SCCs.insert(scc);
1669 int rc=pthread_create(&threads[scc++], NULL,
1670 collect_cycles_in_thread, &arg);
1672 message.status()<<(rc!=0?
"Failure ":
"Success ")
1676 for(
unsigned i=0; i<number_of_sccs; i++)
1677 if(interesting_SCCs.find(i)!=interesting_SCCs.end())
1679 int rc=pthread_join(threads[i], NULL);
1680 message.status()<<(rc!=0?
"Failure ":
"Success ")
std::string get_operation() const
source_locationt source_location
const irep_idt & get_statement() const
data_typet::const_iterator const_iterator
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model, const std::set< event_idt > &filter)
Base class for all expressions.
const source_locationt & source_location() const
The Boolean constant false.
A collection of goto functions.
std::map< irep_idt, goto_functiont > function_mapt
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & code() const
Get the code represented by this instruction.
bool is_set_return_value() const
bool is_end_thread() const
bool is_start_thread() const
bool is_atomic_end() const
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
bool is_atomic_begin() const
std::set< targett, target_less_than > incoming_edges
bool is_function_call() const
const source_locationt & source_location() const
goto_program_instruction_typet type() const
What kind of instruction?
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
instructionst::const_iterator const_targett
std::list< instructiont > instructionst
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
void add_edge(node_indext a, node_indext b)
void visit_cfg_backedge(goto_programt::const_targett targ, goto_programt::const_targett i_it)
strategy: fwd/bwd alternation
void visit_cfg_reference_function(irep_idt id_function)
references the first and last edges of the function
std::set< event_idt > unknown_read_nodes
bool contains_shared_array(const irep_idt &function_id, goto_programt::const_targett targ, goto_programt::const_targett i_it, value_setst &value_sets) const
std::set< event_idt > unknown_write_nodes
instrumentert & instrumenter
void leave_function(const irep_idt &function_id)
virtual void visit_cfg_function(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function_id, std::set< nodet > &ending_vertex)
TODO: move the visitor outside, and inherit.
std::pair< irep_idt, event_idt > id2node_pairt
bool local(const irep_idt &i)
void visit_cfg_fence(goto_programt::instructionst::iterator i_it, const irep_idt &function_id)
void visit_cfg_goto(const irep_idt &function_id, const goto_programt &goto_program, goto_programt::instructionst::iterator i_it, loop_strategyt replicate_body, value_setst &value_sets)
void visit_cfg_function_call(value_setst &value_sets, goto_programt::instructionst::iterator i_it, memory_modelt model, bool no_dependenciess, loop_strategyt duplicate_body)
void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it, const irep_idt &function_id)
void visit_cfg_propagate(goto_programt::instructionst::iterator i_it)
void visit_cfg_assign(value_setst &value_sets, const irep_idt &function_id, goto_programt::instructionst::iterator &i_it, bool no_dependencies)
void visit_cfg(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function_id)
void visit_cfg_duplicate(const goto_programt &goto_program, goto_programt::const_targett targ, goto_programt::const_targett i_it)
void enter_function(const irep_idt &function_id)
void visit_cfg_body(const irep_idt &function_id, const goto_programt &goto_program, goto_programt::const_targett i_it, loop_strategyt replicate_body, value_setst &value_sets)
strategy: fwd/bwd alternation
std::pair< event_idt, event_idt > nodet
void visit_cfg_thread() const
std::set< goto_programt::const_targett, goto_programt::target_less_than > updated
void visit_cfg_skip(goto_programt::instructionst::iterator i_it)
void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it, const irep_idt &function_id)
void print_outputs(memory_modelt model, bool hide_internals)
instrumentert(goto_modelt &_goto_model, messaget &_message)
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
std::set< event_grapht::critical_cyclet > set_of_cycles
std::set< irep_idt > var_to_instr
std::vector< std::set< event_idt > > egraph_SCCs
std::multimap< irep_idt, source_locationt > id2loc
bool is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
goto_functionst & goto_functions
std::map< event_idt, event_idt > map_vertex_gnode
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
void add_instr_to_interleaving(goto_programt::instructionst::iterator it, goto_programt &interleaving)
bool local(const irep_idt &id)
is local variable?
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 print_outputs_local(const std::set< event_grapht::critical_cyclet > &set, std::ofstream &dot, std::ofstream &ref, std::ofstream &output, std::ofstream &all, std::ofstream &table, memory_modelt model, bool hide_internals)
bool get_bool(const irep_idt &name) const
const irep_idt & get_file() const
const irep_idt & get_identifier() const
bool has_prefix(const std::string &s, const std::string &prefix)
void dot(const goto_modelt &src, std::ostream &out)
wmm_grapht::node_indext event_idt
grapht< abstract_eventt > wmm_grapht
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Fences for instrumentation.
event_idt alt_copy_segment(wmm_grapht &alt_egraph, event_idt begin, event_idt end)
#define add_all_pos(it, target, source)
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
dstring_hash irep_id_hash
const std::string & id2string(const irep_idt &d)
Race Detection for Threaded Goto Programs.
#define CHECK_RETURN(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.