Loading...

Searching...

No Matches

Public Member Functions | Public Attributes | Protected Attributes | List of all members

mm_iot Class Reference

+ Collaboration diagram for mm_iot:

[フレーム]

[legend]

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