Add documentation of the mm_io pass in mm_io.h

So that there is an overview of the algorithm used and so that the
relevant markdown file about the related feature is more easily
discoverable.

Author: thomasspriggs

src/goto-programs/mm_io.h

@@ -10,6 +10,21 @@ Date:   April 2017
 
 /// \file
 /// Perform Memory-mapped I/O instrumentation
+///
+/// \details
+/// 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
 
 #ifndef CPROVER_GOTO_PROGRAMS_MM_IO_H
 #define CPROVER_GOTO_PROGRAMS_MM_IO_H