82 if(!race_on_read && !race_on_write)
89 if(race_on_read || race_on_write)
92 original_instruction.
swap(instruction);
104 t_goto->make_goto(t_orig);
105 t_goto->source_location=source_location;
107 t_goto->function=original_instruction.
function;
109 t_call->make_function_call(isr_call);
110 t_call->source_location=source_location;
111 t_call->function=original_instruction.
function;
113 t_orig->
swap(original_instruction);
132 t_goto->make_goto(t_orig);
133 t_goto->source_location=source_location;
135 t_goto->function=i_it->function;
137 t_call->make_function_call(isr_call);
138 t_call->source_location=source_location;
139 t_call->function=i_it->function;
150 std::list<symbol_exprt> matches;
155 symbol_tablet::symbolst::const_iterator s_it=
161 if(s_it->second.type.id()==ID_code)
162 matches.push_back(s_it->second.symbol_expr());
166 throw "interrupt handler `"+
id2string(interrupt_handler)+
"' not found";
168 if(matches.size()>=2)
169 throw "interrupt handler `"+
id2string(interrupt_handler)+
"' is ambiguous";
174 throw "interrupt handler `"+
id2string(interrupt_handler)+
175 "' must not have parameters";
191 value_sets, goto_model, isr);
204 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 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)
typet & type()
Return the type of the expression.
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
A side_effect_exprt that returns a non-deterministically chosen value.
codet representation of a function call statement.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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()
Get the identifier of the entry point to a goto model.
#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)
void swap(instructiont &instruction)
Swap two instructions.
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.