cprover
Loading...
Searching...
No Matches
mm_io.cpp File Reference

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

#include "mm_io.h"
#include <util/fresh_symbol.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <util/pointer_predicates.h>
#include <util/replace_expr.h>
#include "goto_model.h"
#include <set>
+ Include dependency graph for mm_io.cpp:

Go to the source code of this file.

Functions

static std::set< dereference_exprtcollect_deref_expr (const exprt &src)
 
void mm_io (const exprt &mm_io_r, const exprt &mm_io_r_value, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
 
void mm_io (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()

static std::set< dereference_exprt > collect_deref_expr ( const exprt & src)
static

Definition at line 26 of file mm_io.cpp.

◆ mm_io() [1/3]

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

Definition at line 36 of file mm_io.cpp.

◆ mm_io() [2/3]

void mm_io ( goto_modelt & model)

Definition at line 140 of file mm_io.cpp.

◆ mm_io() [3/3]

void mm_io ( symbol_tablet & symbol_table,
goto_functionst & goto_functions )

Definition at line 108 of file mm_io.cpp.