cprover
mm_io.cpp File Reference

Perform Memory-mapped I/O instrumentation. More...

Include dependency graph for mm_io.cpp:

Go to the source code of this file.

Functions

void collect_deref_expr (const exprt &src, std::set< dereference_exprt > &dest)
 
void mm_io (const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
 
void mm_io (const symbol_tablet &symbol_table, goto_functionst &goto_functions)
 
void mm_io (goto_modelt &model)
 

Detailed Description

Perform Memory-mapped I/O instrumentation.

Definition in file mm_io.cpp.

Function Documentation

◆ collect_deref_expr()

void collect_deref_expr ( const exprt src,
std::set< dereference_exprt > &  dest 
)

Definition at line 22 of file mm_io.cpp.

References irept::id(), exprt::operands(), and to_dereference_expr().

Referenced by mm_io().

◆ mm_io() [1/3]

◆ mm_io() [2/3]

void mm_io ( const symbol_tablet symbol_table,
goto_functionst goto_functions 
)

◆ mm_io() [3/3]

void mm_io ( goto_modelt model)

Definition at line 131 of file mm_io.cpp.

References goto_modelt::goto_functions, mm_io(), and goto_modelt::symbol_table.