82 if(!race_on_read && !race_on_write)
89 if(race_on_read || race_on_write)
92 original_instruction.
swap(instruction);
99 isr_call.
function()=interrupt_handler;
105 t_goto->make_goto(t_orig);
106 t_goto->source_location=source_location;
108 t_goto->function=original_instruction.
function;
110 t_call->make_function_call(isr_call);
111 t_call->source_location=source_location;
112 t_call->function=original_instruction.
function;
114 t_orig->
swap(original_instruction);
132 isr_call.
function()=interrupt_handler;
134 t_goto->make_goto(t_orig);
137 t_goto->function=i_it->function;
139 t_call->make_function_call(isr_call);
140 t_call->source_location=source_location;
141 t_call->function=i_it->function;
152 std::list<symbol_exprt> matches;
157 symbol_tablet::symbolst::const_iterator s_it=
163 if(s_it->second.type.id()==ID_code)
164 matches.push_back(s_it->second.symbol_expr());
168 throw "interrupt handler `"+
id2string(interrupt_handler)+
"' not found";
170 if(matches.size()>=2)
171 throw "interrupt handler `"+
id2string(interrupt_handler)+
"' is ambiguous";
176 throw "interrupt handler `"+
id2string(interrupt_handler)+
177 "' must not have parameters";
193 value_sets, goto_model, isr);
206 f_it->second.body, isr, isr_rw_set);
irep_idt function
The function this instruction belongs to.
const std::string & id2string(const irep_idt &d)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const symbol_base_mapt & symbol_base_map
const irep_idt & get_identifier() const
#define forall_rw_set_w_entries(it, rw_set)
symbol_exprt get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
symbol_tablet symbol_table
Symbol table.
This class represents an instruction in the GOTO intermediate representation.
#define forall_rw_set_r_entries(it, rw_set)
instructionst::iterator targett
bool has_r_entry(irep_idt object) const
bool has_w_entry(irep_idt object) const
#define INITIALIZE_FUNCTION
::goto_functiont goto_functiont
targett insert_after(const_targett target)
Insertion after the given target.
A side effect that returns a non-deterministically chosen value.
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 generic container class for the GOTO intermediate representation of one function.
bool potential_race_on_read(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
static irep_idt entry_point()
#define forall_symbol_base_map(it, expr, base_name)
source_locationt source_location
The location of the instruction in the source file.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
void swap(instructiont &instruction)
Swap two instructions.
goto_programt & goto_program
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)
goto_functionst goto_functions
GOTO functions.
Field-insensitive, location-sensitive may-alias analysis.