Make link_to_library independent of the C front-end

Picking the library to load is now left to the tool front-end

jbmc/src/java_bytecode/CMakeLists.txt

@@ -12,4 +12,4 @@ generic_includes(java_bytecode)
 
 # if you link java_bytecode.a in, then you also need to link other .a libraries
 # in
-target_link_libraries(java_bytecode util goto-programs miniz json)
+target_link_libraries(java_bytecode util goto-programs miniz json ansi-c)

src/cbmc/cbmc_parse_options.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 
 #include <ansi-c/c_preprocess.h>
+#include <ansi-c/cprover_library.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
@@ -713,7 +714,7 @@ bool cbmc_parse_optionst::process_goto_program(
     // add the library
     log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
                  << eom;
-    link_to_library(goto_model, log.get_message_handler());
+    link_to_library(goto_model, log.get_message_handler(), add_cprover_library);
 
     if(options.get_bool_option("string-abstraction"))
       string_instrumentation(goto_model, log.get_message_handler());

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -17,6 +17,8 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 
 #include <ansi-c/ansi_c_language.h>
+#include <ansi-c/cprover_library.h>
+
 #include <cpp/cpp_language.h>
 #include <jsil/jsil_language.h>
 
@@ -725,7 +727,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
 
     // add the library
     status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
-    link_to_library(goto_model, ui_message_handler);
+    link_to_library(goto_model, ui_message_handler, add_cprover_library);
     #endif
 
     // remove function pointers

src/goto-diff/goto_diff_parse_options.cpp

@@ -52,6 +52,8 @@ Author: Peter Schrammel
 
 #include <langapi/mode.h>
 
+#include <ansi-c/cprover_library.h>
+
 #include <cbmc/version.h>
 
 #include "goto_diff.h"
@@ -395,7 +397,7 @@ bool goto_diff_parse_optionst::process_goto_program(
 
     // add the library
     status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
-    link_to_library(goto_model, get_message_handler());
+    link_to_library(goto_model, get_message_handler(), add_cprover_library);
 
     // remove function pointers
     status() << "Removal of function pointers and virtual functions" << eom;

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -62,6 +62,8 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/constant_propagator.h>
 #include <analyses/is_threaded.h>
 
+#include <ansi-c/cprover_library.h>
+
 #include <cbmc/version.h>
 
 #include "document_properties.h"
@@ -958,7 +960,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
     // add the library
     status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
-    link_to_library(goto_model, get_message_handler());
+    link_to_library(goto_model, get_message_handler(), add_cprover_library);
   }
 
   // now do full inlining, if requested

src/goto-programs/CMakeLists.txt

@@ -3,5 +3,4 @@ add_library(goto-programs ${sources})
 
 generic_includes(goto-programs)
 
-target_link_libraries(
-        goto-programs util assembler langapi analyses ansi-c)
+target_link_libraries(goto-programs util assembler langapi analyses linking)

src/goto-programs/link_to_library.cpp

@@ -11,27 +11,46 @@ Author: Daniel Kroening, [email protected]
 
 #include "link_to_library.h"
 
-#include <util/config.h>
-
-#include <ansi-c/cprover_library.h>
-
 #include "compute_called_functions.h"
 #include "goto_convert_functions.h"
 
+/// Complete missing function definitions using the \p library.
+/// \param goto_model  goto model that may contain function calls and symbols
+///   with missing function bodies
+/// \param message_handler  message handler to report library processing
+///   problems
+/// \param library  generator function that produces function definitions for a
+///   given set of symbol names that have no body.
 void link_to_library(
   goto_modelt &goto_model,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const std::function<
+    void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)>
+    &library)
 {
   link_to_library(
     goto_model.symbol_table,
     goto_model.goto_functions,
-    message_handler);
+    message_handler,
+    library);
 }
 
+/// Complete missing function definitions using the \p library.
+/// \param symbol_table  symbol table that may contain symbols with missing
+///   function bodies
+/// \param goto_functions  goto functions that may contain function calls with
+///   missing function bodies
+/// \param message_handler  message handler to report library processing
+///   problems
+/// \param library  generator function that produces function definitions for a
+///   given set of symbol names that have no body.
 void link_to_library(
   symbol_tablet &symbol_table,
   goto_functionst &goto_functions,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const std::function<
+    void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)>
+    &library)
 {
   // this needs a fixedpoint, as library functions
   // may depend on other library functions
@@ -69,7 +88,7 @@ void link_to_library(
     if(missing_functions.empty())
       break;
 
-    add_cprover_library(missing_functions, symbol_table, message_handler);
+    library(missing_functions, symbol_table, message_handler);
 
     // convert to CFG
     for(const auto &id : missing_functions)

src/goto-programs/link_to_library.h

@@ -12,17 +12,27 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H
 #define CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H
 
-#include <util/message.h>
+#include <functional>
+#include <set>
 
-#include "goto_model.h"
+#include <util/irep.h>
+
+class goto_functionst;
+class goto_modelt;
+class message_handlert;
+class symbol_tablet;
 
 void link_to_library(
   symbol_tablet &,
   goto_functionst &,
-  message_handlert &);
+  message_handlert &,
+  const std::function<
+    void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)> &);
 
 void link_to_library(
   goto_modelt &,
-  message_handlert &);
+  message_handlert &,
+  const std::function<
+    void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)> &);
 
 #endif // CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H

src/goto-programs/module_dependencies.txt

@@ -1,5 +1,4 @@
 analyses # dubious - concerns call_graph and does_remove_const
-ansi-c # should go away
 assembler # should go away
 goto-programs
 goto-symex # dubious - spurious inclusion of symex_target_equation in graphml_witness