mm_io.cpp File Reference

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

#include "mm_io.h"
#include <util/fresh_symbol.h>
#include <util/message.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.

Classes
class	mm_iot

Functions
static std::set< dereference_exprt >	collect_deref_expr (const exprt &src)
void	mm_io (symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
void	mm_io (goto_modelt &model, message_handlert &message_handler)

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 71 of file mm_io.cpp.

mm_io() [1/2]

void mm_io	(	goto_modelt &	model,
		message_handlert &	message_handler
	)

Definition at line 173 of file mm_io.cpp.

mm_io() [2/2]

void mm_io	(	symbol_tablet &	symbol_table,
		goto_functionst &	goto_functions,
		message_handlert &	message_handler
	)

Definition at line 154 of file mm_io.cpp.