Go to the documentation of this file.
88 if(!race_on_read && !race_on_write)
95 if(race_on_read || race_on_write)
98 original_instruction.
swap(instruction);
117 t_orig->swap(original_instruction);
151 std::list<symbol_exprt> matches;
156 symbol_tablet::symbolst::const_iterator s_it=
157 symbol_table.
symbols.find(m_it->second);
159 if(s_it==symbol_table.
symbols.end())
162 if(s_it->second.type.id()==ID_code)
163 matches.push_back(s_it->second.symbol_expr());
167 throw "interrupt handler '" +
id2string(interrupt_handler) +
"' not found";
169 if(matches.size()>=2)
170 throw "interrupt handler '" +
id2string(interrupt_handler) +
176 throw "interrupt handler '" +
id2string(interrupt_handler) +
177 "' must not have parameters";
193 value_sets, goto_model, isr);
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
source_locationt source_location
The location of the instruction in the source file.
#define forall_rw_set_w_entries(it, rw_set)
static symbol_exprt get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
void swap(instructiont &instruction)
Swap two instructions.
Expression to hold a symbol (variable)
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
typet & type()
Return the type of the expression.
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Interrupt Instrumentation for Goto Programs.
Field-insensitive, location-sensitive may-alias analysis.
const std::string & id2string(const irep_idt &d)
const irep_idt & get_identifier() const
static void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set)
#define forall_rw_set_r_entries(it, rw_set)
#define INITIALIZE_FUNCTION
const parameterst & parameters() const
static bool potential_race_on_read(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
#define Forall_goto_functions(it, functions)
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
bool has_w_entry(irep_idt object) const
goto_functionst goto_functions
GOTO functions.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
#define forall_symbol_base_map(it, expr, base_name)
A generic container class for the GOTO intermediate representation of one function.
bool has_r_entry(irep_idt object) const
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
source_locationt & add_source_location()
This class represents an instruction in the GOTO intermediate representation.
static bool potential_race_on_write(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
symbol_tablet symbol_table
Symbol table.
instructionst::iterator targett