CBMC
|
Memory-mapped I/O Instrumentation for Goto Programs. More...
Go to the source code of this file.
Functions | |
void | mmio (value_setst &, goto_modelt &, message_handlert &) |
Memory-mapped I/O Instrumentation for Goto Programs.
Definition in file mmio.h.
void mmio | ( | value_setst & | value_sets, |
goto_modelt & | goto_model, | ||
message_handlert & | message_handler | ||
) |