cprover
interrupt.cpp File Reference

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

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)
 

Detailed Description

Interrupt Instrumentation.

Definition in file interrupt.cpp.

Function Documentation

◆ get_isr()

symbol_exprt get_isr ( const symbol_tablet symbol_table,
const irep_idt interrupt_handler 
)

◆ interrupt() [1/2]

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 
)

◆ interrupt() [2/2]

void interrupt ( value_setst value_sets,
const symbol_tablet symbol_table,
goto_functionst goto_functions,
const irep_idt interrupt_handler 
)

◆ potential_race_on_read()

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().

◆ potential_race_on_write()

bool potential_race_on_write ( const rw_set_baset code_rw_set,
const rw_set_baset isr_rw_set 
)