cprover
|
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, goto_modelt &goto_model, 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 146 of file interrupt.cpp.
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 53 of file interrupt.cpp.
void interrupt | ( | value_setst & | value_sets, |
goto_modelt & | goto_model, | ||
const irep_idt & | interrupt_handler | ||
) |
Definition at line 180 of file interrupt.cpp.
bool potential_race_on_read | ( | const rw_set_baset & | code_rw_set, |
const rw_set_baset & | isr_rw_set | ||
) |
Definition at line 22 of file interrupt.cpp.
bool potential_race_on_write | ( | const rw_set_baset & | code_rw_set, |
const rw_set_baset & | isr_rw_set | ||
) |
Definition at line 36 of file interrupt.cpp.