CBMC
mmio.cpp File Reference

Memory-mapped I/O Instrumentation for Goto Programs. More...

#include "mmio.h"
#include <linking/static_lifetime_init.h>
#include "rw_set.h"
+ Include dependency graph for mmio.cpp:

Go to the source code of this file.

Functions

static void mmio (value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, message_handlert &message_handler)
 
void mmio (value_setst &value_sets, goto_modelt &goto_model, message_handlert &message_handler)
 

Detailed Description

Memory-mapped I/O Instrumentation for Goto Programs.

Definition in file mmio.cpp.

Function Documentation

◆ mmio() [1/2]

static void mmio ( value_setst value_sets,
const symbol_tablet symbol_table,
const irep_idt function_id,
goto_programt goto_program,
message_handlert message_handler 
)
static

Definition at line 24 of file mmio.cpp.

◆ mmio() [2/2]

void mmio ( value_setst value_sets,
goto_modelt goto_model,
message_handlert message_handler 
)

Definition at line 159 of file mmio.cpp.