mmio.h File Reference

Memory-mapped I/O Instrumentation for Goto Programs. More...

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
void	mmio (value_setst &value_sets, class symbol_tablet &symbol_table, goto_functionst &goto_functions)

Detailed Description

Memory-mapped I/O Instrumentation for Goto Programs.

Definition in file mmio.h.

Function Documentation

mmio()

void mmio	(	value_setst &	value_sets,
		class symbol_tablet &	symbol_table,
		goto_functionst &	goto_functions
	)

Definition at line 165 of file mmio.cpp.

References CPROVER_PREFIX, goto_functions_templatet< goto_programt >::entry_point(), Forall_goto_functions, mmio(), and goto_functions_templatet< bodyT >::update().