C++ front-end now has its own library

Moved new/delete implementation from ansi-c to cpp.

Author: tautschnig

.travis.yml

@@ -286,6 +286,7 @@ install:
   - make -C jbmc/src java-models-library-download
   - make -C src minisat2-download
   - make -C src/ansi-c library_check
+  - make -C src/cpp library_check
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
   - make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -56,6 +56,7 @@ Author: Peter Schrammel
 #include <langapi/mode.h>
 
 #include <ansi-c/cprover_library.h>
+#include <cpp/cprover_library.h>
 
 #include <cbmc/version.h>
 
@@ -342,6 +343,7 @@ bool jdiff_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_cpp_library);
     link_to_library(goto_model, get_message_handler(), add_cprover_c_library);
 
     // remove function pointers

src/cbmc/cbmc_parse_options.cpp

@@ -26,6 +26,8 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/c_preprocess.h>
 #include <ansi-c/cprover_library.h>
 
+#include <cpp/cprover_library.h>
+
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
@@ -714,6 +716,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_cpp_library);
     link_to_library(
       goto_model, log.get_message_handler(), add_cprover_c_library);
 

src/cpp/Makefile

@@ -42,6 +42,7 @@ SRC = cpp_constructor.cpp \
       cpp_typecheck_using.cpp \
       cpp_typecheck_virtual_table.cpp \
       cpp_util.cpp \
+      cprover_library.cpp \
       expr2cpp.cpp \
       parse.cpp \
       template_map.cpp \
@@ -52,11 +53,27 @@ INCLUDES= -I ..
 include ../config.inc
 include ../common
 
-CLEANFILES = cpp$(LIBEXT)
+CLEANFILES = cpp$(LIBEXT) cprover_library.inc library_check
 
 all: cpp$(LIBEXT)
 
 ###############################################################################
 
+../ansi-c/library/converter$(EXEEXT): ../ansi-c/library/converter.cpp
+	$(MAKE) -C ../ansi-c library/converter$(EXEEXT)
+
+library_check: library/*.c
+	./library_check.sh $(CC) $^
+	touch $@
+
+cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c
+	cat library/*.c | ../ansi-c/library/converter$(EXEEXT) > $@
+
+cprover_library.cpp: cprover_library.inc
+
+generated_files: cprover_library.inc
+
+###############################################################################
+
 cpp$(LIBEXT): $(OBJ)
 	$(LINKLIB)

src/cpp/cprover_library.cpp

@@ -0,0 +1,47 @@
+/*******************************************************************\
+
+Module:
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "cprover_library.h"
+
+#include <sstream>
+
+#include <util/config.h>
+
+#include <ansi-c/cprover_library.h>
+
+static std::string get_cprover_library_text(
+  const std::set<irep_idt> &functions,
+  const symbol_tablet &symbol_table)
+{
+  std::ostringstream library_text;
+
+  library_text <<
+    "#line 1 \"<builtin-library>\"\n"
+    "#undef inline\n";
+
+  const struct cprover_library_entryt cprover_library[] =
+#include "cprover_library.inc"
+  ; // NOLINT(whitespace/semicolon)
+
+  return get_cprover_library_text(
+    functions, symbol_table, cprover_library, library_text.str());
+}
+
+void add_cprover_cpp_library(
+  const std::set<irep_idt> &functions,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
+{
+  if(config.ansi_c.lib==configt::ansi_ct::libt::LIB_NONE)
+    return;
+
+  const std::string library_text =
+    get_cprover_library_text(functions, symbol_table);
+
+  add_library(library_text, symbol_table, message_handler);
+}

src/cpp/cprover_library.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module:
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+
+#ifndef CPROVER_CPP_CPROVER_LIBRARY_H
+#define CPROVER_CPP_CPROVER_LIBRARY_H
+
+#include <set>
+
+#include <util/irep.h>
+
+class message_handlert;
+class symbol_tablet;
+
+void add_cprover_cpp_library(
+  const std::set<irep_idt> &functions,
+  symbol_tablet &,
+  message_handlert &);
+
+#endif // CPROVER_CPP_CPROVER_LIBRARY_H

src/ansi-c/library/new.c renamed to src/cpp/library/new.c

@@ -20,6 +20,8 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/cprover_library.h>
 
 #include <cpp/cpp_language.h>
+#include <cpp/cprover_library.h>
+
 #include <jsil/jsil_language.h>
 
 #include <goto-programs/initialize_goto_model.h>
@@ -727,6 +729,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_cpp_library);
     link_to_library(goto_model, ui_message_handler, add_cprover_c_library);
     #endif
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -53,6 +53,7 @@ Author: Peter Schrammel
 #include <langapi/mode.h>
 
 #include <ansi-c/cprover_library.h>
+#include <cpp/cprover_library.h>
 
 #include <cbmc/version.h>
 
@@ -397,6 +398,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_cpp_library);
     link_to_library(goto_model, get_message_handler(), add_cprover_c_library);
 
     // remove function pointers

src/goto-diff/goto_diff_parse_options.cpp

@@ -63,6 +63,7 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/is_threaded.h>
 
 #include <ansi-c/cprover_library.h>
+#include <cpp/cprover_library.h>
 
 #include <cbmc/version.h>
 
@@ -960,6 +961,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_cpp_library);
     link_to_library(goto_model, get_message_handler(), add_cprover_c_library);
   }