CBMC
interrupt.cpp File Reference

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"
+ Include dependency graph for interrupt.cpp:

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)
 

Detailed Description

Interrupt Instrumentation.

Definition in file interrupt.cpp.

Function Documentation

◆ get_isr()

static symbol_exprt get_isr ( const symbol_tablet symbol_table,
const irep_idt interrupt_handler 
)
static

Definition at line 154 of file interrupt.cpp.

◆ interrupt() [1/2]

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

Definition at line 58 of file interrupt.cpp.

◆ interrupt() [2/2]

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.

◆ potential_race_on_read()

static bool potential_race_on_read ( const rw_set_baset code_rw_set,
const rw_set_baset isr_rw_set 
)
static

Definition at line 27 of file interrupt.cpp.

◆ potential_race_on_write()

static bool potential_race_on_write ( const rw_set_baset code_rw_set,
const rw_set_baset isr_rw_set 
)
static

Definition at line 41 of file interrupt.cpp.