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/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.