75 goto_programt::instructiont &instruction=*i_it;
90 if(!race_on_read && !race_on_write)
97 if(race_on_read || race_on_write)
99 goto_programt::instructiont original_instruction;
100 original_instruction.swap(instruction);
103 original_instruction.source_location;
107 isr_call.
function()=interrupt_handler;
113 t_goto->make_goto(t_orig);
114 t_goto->source_location=source_location;
116 t_goto->function=original_instruction.function;
118 t_call->make_function_call(isr_call);
119 t_call->source_location=source_location;
120 t_call->function=original_instruction.function;
122 t_orig->
swap(original_instruction);
140 isr_call.
function()=interrupt_handler;
142 t_goto->make_goto(t_orig);
145 t_goto->function=i_it->function;
147 t_call->make_function_call(isr_call);
148 t_call->source_location=source_location;
149 t_call->function=i_it->function;
160 std::list<symbol_exprt> matches;
165 symbol_tablet::symbolst::const_iterator s_it=
166 symbol_table.
symbols.find(m_it->second);
168 if(s_it==symbol_table.
symbols.end())
171 if(s_it->second.type.id()==ID_code)
172 matches.push_back(s_it->second.symbol_expr());
176 throw "interrupt handler `"+
id2string(interrupt_handler)+
"' not found";
178 if(matches.size()>=2)
179 throw "interrupt handler `"+
id2string(interrupt_handler)+
"' is ambiguous";
184 throw "interrupt handler `"+
id2string(interrupt_handler)+
185 "' must not have parameters";
202 value_sets, ns, goto_functions, isr);
211 value_sets, symbol_table,
215 f_it->second.body, isr, isr_rw_set);
const std::string & id2string(const irep_idt &d)
const irep_idt & get_identifier() const
Goto Programs with Functions.
#define forall_rw_set_w_entries(it, rw_set)
symbol_exprt get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
symbol_base_mapt symbol_base_map
#define forall_rw_set_r_entries(it, rw_set)
bool has_r_entry(irep_idt object) const
bool has_w_entry(irep_idt object) const
static irep_idt entry_point()
API to expression classes.
A side effect that returns a non-deterministically chosen value.
goto_function_templatet< goto_programt > goto_functiont
bool potential_race_on_write(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
Interrupt Instrumentation for Goto Programs.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
bool potential_race_on_read(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
#define forall_symbol_base_map(it, expr, base_name)
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
source_locationt & add_source_location()
void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set)
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
Field-insensitive, location-sensitive may-alias analysis.
instructionst::iterator targett
Race Detection for Threaded Goto Programs.