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/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_exprtcollect_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()

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.