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:

• /home/runner/work/cbmc/cbmc/src/goto-programs/mm_io.cpp