cprover
|
Memory-mapped I/O Instrumentation for Goto Programs. More...
Go to the source code of this file.
Functions | |
void | mmio (value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program) |
void | mmio (value_setst &value_sets, goto_modelt &goto_model) |
Memory-mapped I/O Instrumentation for Goto Programs.
Definition in file mmio.cpp.
void mmio | ( | value_setst & | value_sets, |
const symbol_tablet & | symbol_table, | ||
goto_programt & | goto_program | ||
) |
Definition at line 24 of file mmio.cpp.
References goto_programt::instructiont::code, rw_set_baset::empty(), Forall_goto_program_instructions, goto_program, goto_programt::insert_before(), goto_programt::instructiont::is_assign(), goto_programt::instructiont::make_atomic_begin(), exprt::op1(), goto_programt::instructiont::swap(), shared_bufferst::varst::type, shared_bufferst::varst::w_buff0, and shared_bufferst::varst::w_buff1.
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), and mmio().
void mmio | ( | value_setst & | value_sets, |
goto_modelt & | goto_model | ||
) |
Definition at line 153 of file mmio.cpp.
References goto_functionst::entry_point(), Forall_goto_functions, goto_modelt::goto_functions, INITIALIZE_FUNCTION, mmio(), goto_modelt::symbol_table, and goto_functionst::update().