CBMC
Public Member Functions | Public Attributes | Protected Attributes | List of all members
mm_iot Class Reference
+ Collaboration diagram for mm_iot:

Public Member Functions

 mm_iot (symbol_table_baset &symbol_table)
 
void mm_io (goto_functionst::goto_functiont &goto_function)
 

Public Attributes

std::size_t reads_replaced = 0
 
std::size_t writes_replaced = 0
 

Protected Attributes

const irep_idt id_r = "__CPROVER_" "mm_io_r"
 
const irep_idt id_w = "__CPROVER_" "mm_io_w"
 
const namespacet ns
 
exprt mm_io_r
 
exprt mm_io_r_value
 
exprt mm_io_w
 

Detailed Description

Definition at line 27 of file mm_io.cpp.

Constructor & Destructor Documentation

◆ mm_iot()

mm_iot::mm_iot ( symbol_table_baset &  symbol_table)
explicit

Definition at line 47 of file mm_io.cpp.

Member Function Documentation

◆ mm_io()

void mm_iot::mm_io ( goto_functionst::goto_functiont &  goto_function)

Definition at line 81 of file mm_io.cpp.

Member Data Documentation

◆ id_r

const irep_idt mm_iot::id_r = "__CPROVER_" "mm_io_r"
protected

Definition at line 38 of file mm_io.cpp.

◆ id_w

const irep_idt mm_iot::id_w = "__CPROVER_" "mm_io_w"
protected

Definition at line 39 of file mm_io.cpp.

◆ mm_io_r

exprt mm_iot::mm_io_r
protected

Definition at line 42 of file mm_io.cpp.

◆ mm_io_r_value

exprt mm_iot::mm_io_r_value
protected

Definition at line 43 of file mm_io.cpp.

◆ mm_io_w

exprt mm_iot::mm_io_w
protected

Definition at line 44 of file mm_io.cpp.

◆ ns

const namespacet mm_iot::ns
protected

Definition at line 41 of file mm_io.cpp.

◆ reads_replaced

std::size_t mm_iot::reads_replaced = 0

Definition at line 34 of file mm_io.cpp.

◆ writes_replaced

std::size_t mm_iot::writes_replaced = 0

Definition at line 35 of file mm_io.cpp.

The documentation for this class was generated from the following file: