CBMC
|
Interrupt Instrumentation. More...
#include "interrupt.h"
#include <util/range.h>
#include <util/std_code.h>
#include <linking/static_lifetime_init.h>
#include "rw_set.h"
Go to the source code of this file.
Functions | |
static bool | potential_race_on_read (const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set) |
static bool | potential_race_on_write (const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set) |
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, message_handlert &message_handler) |
static symbol_exprt | get_isr (const symbol_tablet &symbol_table, const irep_idt &interrupt_handler) |
void | interrupt (value_setst &value_sets, goto_modelt &goto_model, const irep_idt &interrupt_handler, message_handlert &message_handler) |
Interrupt Instrumentation.
Definition in file interrupt.cpp.
|
static |
Definition at line 154 of file interrupt.cpp.
|
static |
Definition at line 58 of file interrupt.cpp.
void interrupt | ( | value_setst & | value_sets, |
goto_modelt & | goto_model, | ||
const irep_idt & | interrupt_handler, | ||
message_handlert & | message_handler | ||
) |
Definition at line 188 of file interrupt.cpp.
|
static |
Definition at line 27 of file interrupt.cpp.
|
static |
Definition at line 41 of file interrupt.cpp.