Refactor add_cprover_library to make parts re-usable by the C++ front-end

Author: tautschnig

src/ansi-c/CMakeLists.txt

@@ -50,7 +50,7 @@ add_custom_command(
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
 )
 
-add_custom_target(library_check
+add_custom_target(c_library_check
     DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
 )
 

src/ansi-c/cprover_library.cpp

@@ -14,15 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_language.h"
 
-struct cprover_library_entryt
-{
-  const char *function;
-  const char *model;
-} cprover_library[]=
-#include "cprover_library.inc"
-; // NOLINT(whitespace/semicolon)
-
-std::string get_cprover_library_text(
+static std::string get_cprover_library_text(
   const std::set<irep_idt> &functions,
   const symbol_tablet &symbol_table)
 {
@@ -35,10 +27,29 @@ std::string get_cprover_library_text(
   if(config.ansi_c.string_abstraction)
     library_text << "#define __CPROVER_STRING_ABSTRACTION\n";
 
+  // cprover_library.inc may not have been generated when running Doxygen, thus
+  // make Doxygen skip this part
+  /// \cond
+  const struct cprover_library_entryt cprover_library[] =
+#include "cprover_library.inc"
+    ; // NOLINT(whitespace/semicolon)
+  /// \endcond
+
+  return get_cprover_library_text(
+    functions, symbol_table, cprover_library, library_text.str());
+}
+
+std::string get_cprover_library_text(
+  const std::set<irep_idt> &functions,
+  const symbol_tablet &symbol_table,
+  const struct cprover_library_entryt cprover_library[],
+  const std::string &prologue)
+{
+  std::ostringstream library_text(prologue);
+
   std::size_t count=0;
 
-  for(cprover_library_entryt *e=cprover_library;
-      e->function!=nullptr;
+  for(const cprover_library_entryt *e = cprover_library; e->function != nullptr;
       e++)
   {
     irep_idt id=e->function;
@@ -63,7 +74,7 @@ std::string get_cprover_library_text(
     return library_text.str();
 }
 
-void add_cprover_library(
+void add_cprover_c_library(
   const std::set<irep_idt> &functions,
   symbol_tablet &symbol_table,
   message_handlert &message_handler)

src/ansi-c/cprover_library.h

@@ -15,16 +15,24 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol_table.h>
 #include <util/message.h>
 
+struct cprover_library_entryt
+{
+  const char *function;
+  const char *model;
+};
+
 std::string get_cprover_library_text(
   const std::set<irep_idt> &functions,
-  const symbol_tablet &);
+  const symbol_tablet &,
+  const struct cprover_library_entryt[],
+  const std::string &prologue);
 
 void add_library(
   const std::string &src,
   symbol_tablet &,
   message_handlert &);
 
-void add_cprover_library(
+void add_cprover_c_library(
   const std::set<irep_idt> &functions,
   symbol_tablet &,
   message_handlert &);

src/cbmc/cbmc_parse_options.cpp

@@ -714,7 +714,8 @@ 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(), add_cprover_library);
+    link_to_library(
+      goto_model, log.get_message_handler(), add_cprover_c_library);
 
     if(options.get_bool_option("string-abstraction"))
       string_instrumentation(goto_model, log.get_message_handler());

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -727,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, add_cprover_library);
+    link_to_library(goto_model, ui_message_handler, add_cprover_c_library);
     #endif
 
     // remove function pointers

src/goto-diff/goto_diff_parse_options.cpp

@@ -397,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(), add_cprover_library);
+    link_to_library(goto_model, get_message_handler(), add_cprover_c_library);
 
     // remove function pointers
     status() << "Removal of function pointers and virtual functions" << eom;

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -960,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(), add_cprover_library);
+    link_to_library(goto_model, get_message_handler(), add_cprover_c_library);
   }
 
   // now do full inlining, if requested