Perform Memory-mapped I/O instrumentation. More...
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Functions | |
| void | mm_io (const symbol_tablet &, goto_functionst &, message_handlert &) |
| void | mm_io (goto_modelt &, message_handlert &) |
Detailed Description
Perform Memory-mapped I/O instrumentation.
In the case where a modelling function named __CPROVER_mm_io_r exists in the symbol table, this pass will insert calls to this function before pointer dereference reads. Only the case where there is a single dereference on the right hand side of an assignment is included in the set of dereference reads.
In the case where a modelling function named __CPROVER_mm_io_w exists in the symbol table, this pass will insert calls to this function before all pointer dereference writes. All pointer dereference writes are assumed to be on the left hand side of assignments.
For details as to how and why this is used see the "Device behavior" section of modeling-mmio.md
Definition in file mm_io.h.
Function Documentation
◆ mm_io() [1/2]
| void mm_io | ( | const symbol_tablet & | , |
| goto_functionst & | , | ||
| message_handlert & | |||
| ) |
◆ mm_io() [2/2]
| void mm_io | ( | goto_modelt & | model, |
| message_handlert & | message_handler | ||
| ) |
