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.

◆ mm_io() [1/3]

void mm_io ( const exprt mm_io_r,
const exprt mm_io_w,
goto_functionst::goto_functiont goto_function,
const namespacet ns 
)

Definition at line 32 of file mm_io.cpp.

◆ mm_io() [2/3]

void mm_io ( const symbol_tablet symbol_table,
goto_functionst goto_functions 
)

Definition at line 104 of file mm_io.cpp.

◆ mm_io() [3/3]

void mm_io ( goto_modelt model)

Definition at line 126 of file mm_io.cpp.