cprover
|
Interrupt Instrumentation. More...
#include "interrupt.h"
#include <util/cprover_prefix.h>
#include <util/std_expr.h>
#include <util/std_code.h>
#include <util/prefix.h>
#include <util/symbol_table.h>
#include <goto-programs/goto_functions.h>
#include "rw_set.h"
Go to the source code of this file.
Functions | |
bool | potential_race_on_read (const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set) |
bool | potential_race_on_write (const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set) |
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) |
symbol_exprt | get_isr (const symbol_tablet &symbol_table, const irep_idt &interrupt_handler) |
void | interrupt (value_setst &value_sets, const symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &interrupt_handler) |
Interrupt Instrumentation.
Definition in file interrupt.cpp.
symbol_exprt get_isr | ( | const symbol_tablet & | symbol_table, |
const irep_idt & | interrupt_handler | ||
) |
Definition at line 156 of file interrupt.cpp.
References forall_symbol_base_map, id2string(), symbol_tablet::symbol_base_map, symbol_tablet::symbols, to_code_type(), and exprt::type().
Referenced by interrupt().
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 | ||
) |
Definition at line 61 of file interrupt.cpp.
References exprt::add_source_location(), Forall_goto_program_instructions, code_function_callt::function(), potential_race_on_read(), potential_race_on_write(), exprt::source_location(), and irept::swap().
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), and interrupt().
void interrupt | ( | value_setst & | value_sets, |
const symbol_tablet & | symbol_table, | ||
goto_functionst & | goto_functions, | ||
const irep_idt & | interrupt_handler | ||
) |
Definition at line 190 of file interrupt.cpp.
References CPROVER_PREFIX, goto_functions_templatet< goto_programt >::entry_point(), Forall_goto_functions, symbol_exprt::get_identifier(), get_isr(), interrupt(), and goto_functions_templatet< bodyT >::update().
bool potential_race_on_read | ( | const rw_set_baset & | code_rw_set, |
const rw_set_baset & | isr_rw_set | ||
) |
Definition at line 30 of file interrupt.cpp.
References forall_rw_set_r_entries, and rw_set_baset::has_w_entry().
Referenced by interrupt().
bool potential_race_on_write | ( | const rw_set_baset & | code_rw_set, |
const rw_set_baset & | isr_rw_set | ||
) |
Definition at line 44 of file interrupt.cpp.
References forall_rw_set_w_entries, rw_set_baset::has_r_entry(), and rw_set_baset::has_w_entry().
Referenced by interrupt().