Enable the CPROVER library for goto-analyzer

This does change the functionality quite substantially but strangely it
only seems to affect one test, and that is syntactic rather than semantic.
As with many of the other changes in this PR, I suspect this is swapping
one lot of broken, untested functionality for another, slightly less broken
but still not working lot of functionality.

Author: martin

regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc

@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removing function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF fp == f1 THEN GOTO [0-9]+$
+^\s*IF fp == f2 THEN GOTO [0-9]+$
+^\s*IF fp == f3 THEN GOTO [0-9]+$
+^\s*IF fp == f4 THEN GOTO [0-9]+$
+^\s*IF fp == f5 THEN GOTO [0-9]+$
+^\s*IF fp == f6 THEN GOTO [0-9]+$
+^\s*IF fp == f7 THEN GOTO [0-9]+$
+^\s*IF fp == f8 THEN GOTO [0-9]+$
+^\s*IF fp == f9 THEN GOTO [0-9]+$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -31,6 +31,7 @@ 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/process_goto_program.h>
 #include <goto-programs/read_goto_binary.h>
@@ -876,25 +877,23 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     // adding the library.
     remove_asm(goto_model);
 
-#if 0
     // add the library
     log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << messaget::eom;
     link_to_library(
       goto_model, ui_message_handler, cprover_cpp_library_factory);
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
 
-    // these are commented out as well because without the library
-    // this initialization code doesn’t make any sense
     add_malloc_may_fail_variable_initializations(goto_model);
 
-#endif
-
     // remove function pointers
     log.status() << "Removing function pointers and virtual functions"
                  << messaget::eom;
     remove_function_pointers(
       ui_message_handler, goto_model, cmdline.isset("pointer-check"));
 
+    // instrument library preconditions
+    instrument_preconditions(goto_model);
+
     // do partial inlining
     log.status() << "Partial Inlining" << messaget::eom;
     goto_partial_inline(goto_model, ui_message_handler);