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
	)

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

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
	)

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

interrupt() [2/2]

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

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
	)

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