Add memory mapped IO support to goto-analyzer

This does add functionality but it is of the "used to be silently ignored
but now sort of works or maybe breaks" kind.

Author: martin

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -31,7 +31,9 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/link_to_library.h>
+#include <goto-programs/mm_io.h>
 #include <goto-programs/process_goto_program.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_complex.h>
@@ -898,6 +900,11 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     remove_function_pointers(
       ui_message_handler, goto_model, options.get_bool_option("pointer-check"));
 
+    mm_io(goto_model);
+
+    // instrument library preconditions
+    instrument_preconditions(goto_model);
+
     // do partial inlining
     log.status() << "Partial Inlining" << messaget::eom;
     goto_partial_inline(goto_model, ui_message_handler);