#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 "remove_returns.h"
#include <set>

Include dependency graph for mm_io.cpp:

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_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()

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

Definition at line 27 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 37 of file mm_io.cpp.

◆ mm_io() [2/3]

void mm_io ( goto_modelt & model )

Definition at line 145 of file mm_io.cpp.

◆ mm_io() [3/3]

void mm_io	(	symbol_tablet &	symbol_table,
		goto_functionst &	goto_functions
	)