32 #define OUTPUT(s, fence, file, line, id, type) \ 33 s<<fence<<"|"<<file<<"|"<<line<<"|"<<id<<"|"<<type<<'\n' 58 std::set<std::string> non_redundant_display;
60 for(std::list<symbol_exprt>::const_iterator it=
fenced_edges.writes.begin();
66 if(it->source_location().as_string().empty())
72 it->source_location().get_file(),
73 it->source_location().get_line(),
74 ns.
lookup(it->get_identifier()).base_name,
76 non_redundant_display.insert(s.str());
79 for(std::list<symbol_exprt>::const_iterator it=
fenced_edges.reads.begin();
85 if(it->source_location().as_string().empty())
91 it->source_location().get_file(),
92 it->source_location().get_line(),
93 ns.
lookup(it->get_identifier()).base_name,
95 non_redundant_display.insert(s.str());
98 std::ofstream results;
99 results.open(
"results.txt");
100 for(std::set<std::string>::const_iterator it=non_redundant_display.begin();
101 it!=non_redundant_display.end();
113 :message(_message), value_sets(_value_sets), symbol_table(_symbol_table),
114 ns(_symbol_table), goto_functions(_goto_functions)
191 if(src.
id()==ID_symbol)
193 symbol_tablet::symbolst::const_iterator s_it=
210 for(typet::subtypest::const_iterator it=src.
subtypes().begin();
227 std::cout <<
"--------\n";
256 fenced_edges.writes.push_front(w_it->second.symbol_expr);
284 fenced_edges.reads.push_front(r_it->second.symbol_expr);
287 catch (std::string s)
300 std::cout <<
"--------\n";
310 if(i_it->is_function_call())
328 <<
" loc: " << w_it->second.symbol_expr.source_location()
334 std::map<const irep_idt, const irep_idt> &ref=
336 if(ref.find(w_it->second.object)!=ref.end())
338 const irep_idt from=ref[w_it->second.object];
351 <<
id2string(w_it->second.object) <<
" -> " 353 fenced_edges.writes.push_front(w_it->second.symbol_expr);
373 <<
id2string(r_it->second.object) <<
" shared: " 375 << r_it->second.symbol_expr.source_location() <<
messaget::eom;
380 std::map<const irep_idt, const irep_idt>&
382 if(ref.find(r_it->second.object)!=ref.end())
384 const irep_idt from=ref[r_it->second.object];
398 <<
id2string(r_it->second.object) <<
" -> " 400 fenced_edges.reads.push_front(r_it->second.symbol_expr);
425 fence_all_shared_aeg_explore(main.
body 441 if(i_it->is_function_call())
450 if(visited_functions.find(fun_id)!=visited_functions.end())
453 visited_functions.insert(fun_id);
454 fence_all_shared_aeg_explore(
460 visited_functions.erase(fun_id);
477 <<
id2string(w_it->second.object) <<
" shared: " 479 << w_it->second.symbol_expr.source_location() <<
messaget::eom;
484 std::map<const irep_idt, const irep_idt>&
486 if(ref.find(w_it->second.object)!=ref.end())
488 const irep_idt from=ref[w_it->second.object];
502 <<
id2string(w_it->second.object) <<
" -> " 504 fenced_edges.writes.push_front(w_it->second.symbol_expr);
524 <<
id2string(r_it->second.object) <<
" shared: " 526 << r_it->second.symbol_expr.source_location() <<
messaget::eom;
531 std::map<const irep_idt, const irep_idt>&
533 if(ref.find(r_it->second.object)!=ref.end())
535 const irep_idt from=ref[r_it->second.object];
549 <<
id2string(r_it->second.object) <<
" -> " 551 fenced_edges.reads.push_front(r_it->second.symbol_expr);
574 instrumenter.
do_it();
586 instrumenter.
do_it();
598 instrumenter.
do_it();
The type of an expression.
bool has_subtypes() const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
fence_all_shared_aegt(messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
const irep_idt & get_identifier() const
Goto Programs with Functions.
void fence_all_shared_aeg(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
#define forall_rw_set_w_entries(it, rw_set)
std::list< symbol_exprt > reads
std::map< const irep_idt, const irep_idt > dereferenced_from
void fence_volatile(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
bool get_bool(const irep_namet &name) const
#define OUTPUT(s, fence, file, line, id, type)
const irep_idt & id() const
#define forall_rw_set_r_entries(it, rw_set)
const symbol_tablet & symbol_table
std::list< symbol_exprt > writes
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
std::set< irep_idt > visited_functions
static irep_idt entry_point()
std::set< irep_idt > set_reads
function_mapt function_map
simple_insertiont(messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
bool has_prefix(const std::string &s, const std::string &prefix)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
bool is_volatile(const typet &src) const
we can determine whether an access is volatile just by looking at the type of the variables involved ...
struct simple_insertiont::@17 fenced_edges
const typet & subtype() const
void print_to_file() const
#define forall_goto_functions(it, functions)
fence_volatilet(messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
virtual ~simple_insertiont()
#define forall_goto_program_instructions(it, program)
const goto_functionst & goto_functions
bool is_volatile(const symbol_tablet &symbol_table, const typet &src)
void fence_all_shared_aeg_explore(const goto_programt &code)
fence_all_sharedt(messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
Field-insensitive, location-sensitive may-alias analysis.
const code_function_callt & to_code_function_call(const codet &code)
void fence_all_shared(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
Race Detection for Threaded Goto Programs.