From d597d9029f04bb1df3ed7429c4d316bb7871fcf1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 6 Jun 2018 17:28:00 +0000 Subject: [PATCH 1/8] Remove unused include --- jbmc/src/janalyzer/janalyzer_parse_options.cpp | 1 - src/clobber/clobber_parse_options.cpp | 1 - 2 files changed, 2 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 21c93527c0a..243ca8682b5 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 0d0c637c75d..0ee4ad81fee 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -27,7 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include From c471f72b00de5b5a62d0ed8824996cf3cda886ec Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jun 2018 08:01:49 +0000 Subject: [PATCH 2/8] jdiff: remove C library jdiff only supports the java_bytecode language. --- jbmc/src/jdiff/jdiff_parse_options.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 5cf3135aba6..402123877fa 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -338,9 +338,6 @@ bool jdiff_parse_optionst::process_goto_program( { try { - // add the library - link_to_library(goto_model, get_message_handler()); - // remove function pointers status() << "Removal of function pointers and virtual functions" << eom; remove_function_pointers( From c8702ab66eed1db8c60a9f7b82d066ee8648d061 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 6 Jun 2018 17:28:46 +0000 Subject: [PATCH 3/8] CPROVER library linking: move status message to front-end --- src/cbmc/cbmc_parse_options.cpp | 2 ++ src/goto-analyzer/goto_analyzer_parse_options.cpp | 1 + src/goto-diff/goto_diff_parse_options.cpp | 1 + src/goto-instrument/goto_instrument_parse_options.cpp | 1 + src/goto-programs/link_to_library.cpp | 5 ----- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 9411a1b8c37..2c93be02896 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -711,6 +711,8 @@ bool cbmc_parse_optionst::process_goto_program( remove_asm(goto_model); // add the library + log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" + << eom; link_to_library(goto_model, log.get_message_handler()); if(options.get_bool_option("string-abstraction")) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 7022fc3d771..d557842dda7 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -724,6 +724,7 @@ bool goto_analyzer_parse_optionst::process_goto_program( remove_asm(goto_model); // add the library + status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom; link_to_library(goto_model, ui_message_handler); #endif diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 4fae66c5650..81fd4448be8 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -394,6 +394,7 @@ bool goto_diff_parse_optionst::process_goto_program( remove_asm(goto_model); // add the library + status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom; link_to_library(goto_model, get_message_handler()); // remove function pointers diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 2b80bd3969a..d54c80ba37a 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -957,6 +957,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS"); // add the library + status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom; link_to_library(goto_model, get_message_handler()); } diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 05b7a863059..856d8d12495 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -36,11 +36,6 @@ void link_to_library( // this needs a fixedpoint, as library functions // may depend on other library functions - messaget message(message_handler); - - message.status() << "Adding CPROVER library (" - << config.ansi_c.arch << ")" << messaget::eom; - std::set added_functions; while(true) From 0ea614360234c895a04722ef2e477e89bbb257d1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 6 Jun 2018 18:10:21 +0000 Subject: [PATCH 4/8] 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 | 2 +- src/cbmc/cbmc_parse_options.cpp | 3 +- .../goto_analyzer_parse_options.cpp | 4 ++- src/goto-diff/goto_diff_parse_options.cpp | 4 ++- .../goto_instrument_parse_options.cpp | 4 ++- src/goto-programs/CMakeLists.txt | 3 +- src/goto-programs/link_to_library.cpp | 35 ++++++++++++++----- src/goto-programs/link_to_library.h | 18 +++++++--- src/goto-programs/module_dependencies.txt | 1 - 9 files changed, 54 insertions(+), 20 deletions(-) diff --git a/jbmc/src/java_bytecode/CMakeLists.txt b/jbmc/src/java_bytecode/CMakeLists.txt index 6fd4d77a666..8eb497341bf 100644 --- a/jbmc/src/java_bytecode/CMakeLists.txt +++ b/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) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 2c93be02896..2f680b478cb 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -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()); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index d557842dda7..fe95da32ab3 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include @@ -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 diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 81fd4448be8..48fa3f83b9d 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -52,6 +52,8 @@ Author: Peter Schrammel #include +#include + #include #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; diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index d54c80ba37a..2ca115462d2 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -62,6 +62,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #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 diff --git a/src/goto-programs/CMakeLists.txt b/src/goto-programs/CMakeLists.txt index 6f00811ad4f..ab2e8a0543c 100644 --- a/src/goto-programs/CMakeLists.txt +++ b/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) diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index 856d8d12495..3559b36ae5d 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -11,27 +11,46 @@ Author: Daniel Kroening, kroening@kroening.com #include "link_to_library.h" -#include - -#include - #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 &, 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 &, 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) diff --git a/src/goto-programs/link_to_library.h b/src/goto-programs/link_to_library.h index c45c5efbfa2..495c43de244 100644 --- a/src/goto-programs/link_to_library.h +++ b/src/goto-programs/link_to_library.h @@ -12,17 +12,27 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H #define CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H -#include +#include +#include -#include "goto_model.h" +#include + +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 &, symbol_tablet &, message_handlert &)> &); void link_to_library( goto_modelt &, - message_handlert &); + message_handlert &, + const std::function< + void(const std::set &, symbol_tablet &, message_handlert &)> &); #endif // CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H diff --git a/src/goto-programs/module_dependencies.txt b/src/goto-programs/module_dependencies.txt index 2b7d86a1a36..bfdc19df2c8 100644 --- a/src/goto-programs/module_dependencies.txt +++ b/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 From ed05d3e0801e84aad50d5242ad527c91c5dcd038 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 6 Jun 2018 18:12:58 +0000 Subject: [PATCH 5/8] Refactor add_cprover_library to make parts re-usable by the C++ front-end --- src/ansi-c/CMakeLists.txt | 2 +- src/ansi-c/cprover_library.cpp | 35 ++++++++++++------- src/ansi-c/cprover_library.h | 12 +++++-- src/cbmc/cbmc_parse_options.cpp | 3 +- .../goto_analyzer_parse_options.cpp | 2 +- src/goto-diff/goto_diff_parse_options.cpp | 2 +- .../goto_instrument_parse_options.cpp | 2 +- 7 files changed, 39 insertions(+), 19 deletions(-) diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt index 43c38d3999f..0695c17025d 100644 --- a/src/ansi-c/CMakeLists.txt +++ b/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 ) diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index f13e321d752..895e35809fb 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -14,15 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #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 &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 &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 &functions, symbol_tablet &symbol_table, message_handlert &message_handler) diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h index 6f36eb5abca..ed9587cd767 100644 --- a/src/ansi-c/cprover_library.h +++ b/src/ansi-c/cprover_library.h @@ -15,16 +15,24 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +struct cprover_library_entryt +{ + const char *function; + const char *model; +}; + std::string get_cprover_library_text( const std::set &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 &functions, symbol_tablet &, message_handlert &); diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 2f680b478cb..d967fd14470 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/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()); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index fe95da32ab3..726dc675909 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/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 diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 48fa3f83b9d..12d4c11abd9 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/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; diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 2ca115462d2..fdb6f43f356 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/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 From 0451f1e7f7b03814dc021c68663a460eca8236e8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jun 2018 07:47:39 +0000 Subject: [PATCH 6/8] C++ front-end now has its own library Moved new/delete implementation from ansi-c to cpp. --- .gitignore | 1 + .travis.yml | 1 + src/cbmc/cbmc_parse_options.cpp | 4 ++ src/cpp/CMakeLists.txt | 30 +++++++++++ src/cpp/Makefile | 19 ++++++- src/cpp/cprover_library.cpp | 50 ++++++++++++++++++ src/cpp/cprover_library.h | 24 +++++++++ src/cpp/library/cprover.h | 52 +++++++++++++++++++ src/cpp/library/module_dependencies.txt | 2 + src/{ansi-c => cpp}/library/new.c | 0 .../goto_analyzer_parse_options.cpp | 3 ++ src/goto-diff/goto_diff_parse_options.cpp | 2 + .../goto_instrument_parse_options.cpp | 2 + 13 files changed, 189 insertions(+), 1 deletion(-) create mode 100644 src/cpp/cprover_library.cpp create mode 100644 src/cpp/cprover_library.h create mode 100644 src/cpp/library/cprover.h create mode 100644 src/cpp/library/module_dependencies.txt rename src/{ansi-c => cpp}/library/new.c (100%) diff --git a/.gitignore b/.gitignore index 1627be3e149..822bd06e8bc 100644 --- a/.gitignore +++ b/.gitignore @@ -49,6 +49,7 @@ src/ansi-c/gcc_builtin_headers_mips.inc src/ansi-c/gcc_builtin_headers_power.inc src/ansi-c/gcc_builtin_headers_ubsan.inc src/ansi-c/windows_builtin_headers.inc +src/cpp/cprover_library.inc # regression/test files *.out diff --git a/.travis.yml b/.travis.yml index 3d8662f80d8..b43c014a5c3 100644 --- a/.travis.yml +++ b/.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 diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index d967fd14470..e2ab0fac1d5 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -26,6 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include #include @@ -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); diff --git a/src/cpp/CMakeLists.txt b/src/cpp/CMakeLists.txt index b4d00b13a21..8054ba23c7d 100644 --- a/src/cpp/CMakeLists.txt +++ b/src/cpp/CMakeLists.txt @@ -1,3 +1,33 @@ +file(GLOB cpp_library_sources "library/*.c") + +add_custom_command(OUTPUT converter_input.txt + COMMAND cat ${cpp_library_sources} > converter_input.txt + DEPENDS ${cpp_library_sources} +) + +add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc" + COMMAND ../ansi-c/converter < "converter_input.txt" > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc" + DEPENDS "converter_input.txt" ../ansi-c/converter +) + +################################################################################ + +file(GLOB library_check_sources "library/*.c") + +add_custom_command( + DEPENDS ${library_check_sources} + COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/../ansi-c/library_check.sh ${CMAKE_C_COMPILER} ${library_check_sources} + COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp + OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} +) + +add_custom_target(cpp_library_check + DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp +) + +################################################################################ + file(GLOB_RECURSE sources "*.cpp" "*.h") add_library(cpp ${sources}) diff --git a/src/cpp/Makefile b/src/cpp/Makefile index b98e4766b42..bad4f4030c1 100644 --- a/src/cpp/Makefile +++ b/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 + ../ansi-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) diff --git a/src/cpp/cprover_library.cpp b/src/cpp/cprover_library.cpp new file mode 100644 index 00000000000..765f03555ad --- /dev/null +++ b/src/cpp/cprover_library.cpp @@ -0,0 +1,50 @@ +/*******************************************************************\ + +Module: + +Author: Michael Tautschnig + +\*******************************************************************/ + +#include "cprover_library.h" + +#include + +#include + +#include + +static std::string get_cprover_library_text( + const std::set &functions, + const symbol_tablet &symbol_table) +{ + std::ostringstream library_text; + + library_text << "#line 1 \"\"\n" + << "#undef inline\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()); +} + +void add_cprover_cpp_library( + const std::set &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); +} diff --git a/src/cpp/cprover_library.h b/src/cpp/cprover_library.h new file mode 100644 index 00000000000..9c9e76a7fe7 --- /dev/null +++ b/src/cpp/cprover_library.h @@ -0,0 +1,24 @@ +/*******************************************************************\ + +Module: + +Author: Michael Tautschnig + +\*******************************************************************/ + +#ifndef CPROVER_CPP_CPROVER_LIBRARY_H +#define CPROVER_CPP_CPROVER_LIBRARY_H + +#include + +#include + +class message_handlert; +class symbol_tablet; + +void add_cprover_cpp_library( + const std::set &functions, + symbol_tablet &, + message_handlert &); + +#endif // CPROVER_CPP_CPROVER_LIBRARY_H diff --git a/src/cpp/library/cprover.h b/src/cpp/library/cprover.h new file mode 100644 index 00000000000..d4a3b53fc7e --- /dev/null +++ b/src/cpp/library/cprover.h @@ -0,0 +1,52 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_CPP_LIBRARY_CPROVER_H +#define CPROVER_CPP_LIBRARY_CPROVER_H + +// NOLINTNEXTLINE(readability/identifiers) +typedef __typeof__(sizeof(int)) __CPROVER_size_t; +void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero); +extern const void *__CPROVER_deallocated; +extern const void *__CPROVER_malloc_object; +extern __CPROVER_size_t __CPROVER_malloc_size; +extern _Bool __CPROVER_malloc_is_new_array; +extern const void *__CPROVER_memory_leak; + +void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__)); +void __CPROVER_assert(__CPROVER_bool assertion, const char *description); +void __CPROVER_precondition(__CPROVER_bool assertion, const char *description); + +void __CPROVER_input(const char *id, ...); +void __CPROVER_output(const char *id, ...); + +// concurrency-related +void __CPROVER_atomic_begin(); +void __CPROVER_atomic_end(); +void __CPROVER_fence(const char *kind, ...); + +// pointers +unsigned __CPROVER_POINTER_OBJECT(const void *p); +signed __CPROVER_POINTER_OFFSET(const void *p); +__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p); + +// arrays +// __CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2); +void __CPROVER_array_copy(const void *dest, const void *src); +void __CPROVER_array_set(const void *dest, ...); +void __CPROVER_array_replace(const void *dest, const void *src); + +void __CPROVER_set_must(const void *, const char *); +void __CPROVER_set_may(const void *, const char *); +void __CPROVER_clear_must(const void *, const char *); +void __CPROVER_clear_may(const void *, const char *); +void __CPROVER_cleanup(const void *, void (*)(void *)); +__CPROVER_bool __CPROVER_get_must(const void *, const char *); +__CPROVER_bool __CPROVER_get_may(const void *, const char *); + +#endif // CPROVER_CPP_LIBRARY_CPROVER_H diff --git a/src/cpp/library/module_dependencies.txt b/src/cpp/library/module_dependencies.txt new file mode 100644 index 00000000000..b88507e18e4 --- /dev/null +++ b/src/cpp/library/module_dependencies.txt @@ -0,0 +1,2 @@ +cpp +cpp/library diff --git a/src/ansi-c/library/new.c b/src/cpp/library/new.c similarity index 100% rename from src/ansi-c/library/new.c rename to src/cpp/library/new.c diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 726dc675909..3493b8cd9a0 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include @@ -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 diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 12d4c11abd9..f8f4b50dc46 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -53,6 +53,7 @@ Author: Peter Schrammel #include #include +#include #include @@ -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 diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index fdb6f43f356..1f863c6a2fd 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -63,6 +63,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -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); } From 1201ffe947f4b0ca63c208608d3036ecd2288003 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 Aug 2017 09:11:11 +0100 Subject: [PATCH 7/8] C++ front-end: Use C factory for compiler builtins --- src/cpp/cpp_internal_additions.cpp | 163 +++++++++++++++-------------- src/cpp/cpp_typecheck.cpp | 6 ++ src/cpp/cpp_typecheck.h | 2 + src/cpp/cpp_typecheck_resolve.cpp | 12 +++ 4 files changed, 107 insertions(+), 76 deletions(-) diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 2c3d33a00d6..9f733c6abab 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -42,23 +42,7 @@ std::string c2cpp(const std::string &s) void cpp_internal_additions(std::ostream &out) { - out << "# 1 \"\"" << '\n'; - - // new and delete are in the root namespace! - out << "void operator delete(void *);" << '\n'; - out << "void *operator new(__typeof__(sizeof(int)));" << '\n'; - - // auxiliaries for new/delete - out << "extern \"C\" void *__new(__typeof__(sizeof(int)));" << '\n'; - // NOLINTNEXTLINE(whitespace/line_length) - out << "extern \"C\" void *__new_array(__typeof__(sizeof(int)), __typeof__(sizeof(int)));" << '\n'; - // NOLINTNEXTLINE(whitespace/line_length) - out << "extern \"C\" void *__placement_new(__typeof__(sizeof(int)), void *);" << '\n'; - // NOLINTNEXTLINE(whitespace/line_length) - out << "extern \"C\" void *__placement_new_array(__typeof__(sizeof(int)), __typeof__(sizeof(int)), void *);" << '\n'; - out << "extern \"C\" void __delete(void *);" << '\n'; - out << "extern \"C\" void __delete_array(void *);" << '\n'; - out << "extern \"C\" bool __CPROVER_malloc_is_new_array=0;" << '\n'; + out << "# 1 \"\"" << '\n'; // __CPROVER namespace out << "namespace __CPROVER { }" << '\n'; @@ -71,84 +55,111 @@ void cpp_internal_additions(std::ostream &out) << " __CPROVER::ssize_t;" << '\n'; out << "typedef __CPROVER::ssize_t __CPROVER_ssize_t;" << '\n'; - // assume/assert - out << "extern \"C\" void assert(bool assertion);" << '\n'; - out << "extern \"C\" void __CPROVER_assume(bool assumption);" << '\n'; - out << "extern \"C\" void __CPROVER_assert(" - "bool assertion, const char *description);" << '\n'; - out << "extern \"C\" void __CPROVER::assume(bool assumption);" << '\n'; - out << "extern \"C\" void __CPROVER::assert(" - "bool assertion, const char *description);" << '\n'; + // new and delete are in the root namespace! + out << "void operator delete(void *);" << '\n'; + out << "void *operator new(__CPROVER::size_t);" << '\n'; + + out << "extern \"C\" {" << '\n'; // CPROVER extensions - out << "extern \"C\" const unsigned __CPROVER::constant_infinity_uint;\n"; - out << "extern \"C\" void " INITIALIZE_FUNCTION "();" << '\n'; - out << "extern \"C\" void __CPROVER::input(const char *id, ...);" << '\n'; - out << "extern \"C\" void __CPROVER::output(const char *id, ...);" << '\n'; - out << "extern \"C\" void __CPROVER::cover(bool condition);" << '\n'; - out << "extern \"C\" void __CPROVER::atomic_begin();" << '\n'; - out << "extern \"C\" void __CPROVER::atomic_end();" << '\n'; - - // pointers - out << "extern \"C\" __CPROVER::size_t __CPROVER_POINTER_OBJECT(const void *);\n"; - out << "extern \"C\" __CPROVER::ssize_t __CPROVER_POINTER_OFFSET(const void *);" << '\n'; - out << "extern \"C\" bool __CPROVER_DYNAMIC_OBJECT(const void *p);" << '\n'; - // NOLINTNEXTLINE(whitespace/line_length) - out << "extern \"C\" extern unsigned char __CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n'; - out << "extern \"C\" const void *__CPROVER_dead_object=0;" << '\n'; + out << "const unsigned __CPROVER::constant_infinity_uint;" << '\n'; + out << "typedef void __CPROVER_integer;" << '\n'; + out << "typedef void __CPROVER_rational;" << '\n'; + // TODO + // out << "thread_local unsigned long __CPROVER_thread_id = 0;" << '\n'; + out << "__CPROVER_bool " + << "__CPROVER_threads_exited[__CPROVER::constant_infinity_uint];" << '\n'; + out << "unsigned long __CPROVER_next_thread_id = 0;" << '\n'; + out << "extern unsigned char " + << "__CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n'; // malloc - out << "extern \"C\" void *__CPROVER_allocate(__CPROVER_size_t size," - << " __CPROVER_bool zero);" << '\n'; - out << "extern \"C\" const void *__CPROVER_deallocated=0;" << '\n'; - out << "extern \"C\" const void *__CPROVER_malloc_object=0;" << '\n'; - out << "extern \"C\" __CPROVER::size_t __CPROVER_malloc_size;" << '\n'; + out << "const void *__CPROVER_deallocated = 0;" << '\n'; + out << "const void *__CPROVER_dead_object = 0;" << '\n'; + out << "const void *__CPROVER_malloc_object = 0;" << '\n'; + out << "__CPROVER::size_t __CPROVER_malloc_size;" << '\n'; + out << "__CPROVER_bool __CPROVER_malloc_is_new_array = 0;" << '\n'; + out << "const void *__CPROVER_memory_leak = 0;" << '\n'; + out << "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);" + << '\n'; - // float - out << "extern \"C\" int __CPROVER_rounding_mode;" << '\n'; - - // arrays - // NOLINTNEXTLINE(whitespace/line_length) - out << "bool __CPROVER::array_equal(const void array1[], const void array2[]);" << '\n'; - out << "void __CPROVER::array_copy(const void dest[], const void src[]);\n"; - out << "void __CPROVER::array_set(const void dest[], ...);" << '\n'; + // auxiliaries for new/delete + out << "void *__new(__CPROVER::size_t);" << '\n'; + out << "void *__new_array(__CPROVER::size_t, __CPROVER::size_t);" << '\n'; + out << "void *__placement_new(__CPROVER::size_t, void *);" << '\n'; + out << "void *__placement_new_array(" + << "__CPROVER::size_t, __CPROVER::size_t, void *);" << '\n'; + out << "void __delete(void *);" << '\n'; + out << "void __delete_array(void *);" << '\n'; - // GCC stuff, but also for ARM + // float + // TODO: should the thread_local + out << "int __CPROVER_rounding_mode = " + << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n'; + + // pipes, write, read, close + out << "struct __CPROVER_pipet {\n" + << " bool widowed;\n" + << " char data[4];\n" + << " short next_avail;\n" + << " short next_unread;\n" + << "};\n"; + out << "extern struct __CPROVER_pipet " + << "__CPROVER_pipes[__CPROVER::constant_infinity_uint];" << '\n'; + // offset to make sure we don't collide with other fds + out << "extern const int __CPROVER_pipe_offset;" << '\n'; + out << "unsigned __CPROVER_pipe_count=0;" << '\n'; + + // This function needs to be declared, or otherwise can't be called + // by the entry-point construction. + out << "void " INITIALIZE_FUNCTION "();" << '\n'; + + // GCC junk stuff, also for CLANG and ARM if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC || config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE || config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) { - out << "extern \"C\" {" << '\n'; out << c2cpp(gcc_builtin_headers_types); - out << c2cpp(gcc_builtin_headers_generic); - out << c2cpp(gcc_builtin_headers_math); - out << c2cpp(gcc_builtin_headers_mem_string); - out << c2cpp(gcc_builtin_headers_omp); - out << c2cpp(gcc_builtin_headers_tm); - out << c2cpp(gcc_builtin_headers_ubsan); - out << c2cpp(clang_builtin_headers); - - if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE) - out << "typedef double __float128;\n"; // clang doesn't do __float128 - - out << c2cpp(gcc_builtin_headers_ia32); - out << c2cpp(gcc_builtin_headers_ia32_2); - out << c2cpp(gcc_builtin_headers_ia32_3); - out << c2cpp(gcc_builtin_headers_ia32_4); - out << "}" << '\n'; + + if( + config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" || + config.ansi_c.arch == "x32") + { + // clang doesn't do __float128 + if(config.ansi_c.mode == configt::ansi_ct::flavourt::APPLE) + out << "typedef double __float128;" << '\n'; + } + + // On 64-bit systems, gcc has typedefs + // __int128_t und __uint128_t -- but not on 32 bit! + if(config.ansi_c.long_int_width >= 64) + { + out << "typedef signed __int128 __int128_t;" << '\n'; + out << "typedef unsigned __int128 __uint128_t;" << '\n'; + } } - // extensions for Visual C/C++ + // this is Visual C/C++ only if(config.ansi_c.os==configt::ansi_ct::ost::OS_WIN) - out << "extern \"C\" int __noop(...);\n"; + { + out << "int __noop(...);" << '\n'; + out << "int __assume(int);" << '\n'; + } + + // ARM stuff + if(config.ansi_c.mode == configt::ansi_ct::flavourt::ARM) + out << c2cpp(arm_builtin_headers); + + // CW stuff + if(config.ansi_c.mode == configt::ansi_ct::flavourt::CODEWARRIOR) + out << c2cpp(cw_builtin_headers); // string symbols to identify the architecture we have compiled for std::string architecture_strings; ansi_c_architecture_strings(architecture_strings); + out << c2cpp(architecture_strings); - out << "extern \"C\" {" << '\n'; - out << architecture_strings; - out << "}" << '\n'; + out << '}' << '\n'; // end extern "C" // Microsoft stuff if(config.ansi_c.mode==configt::ansi_ct::flavourt::VISUAL_STUDIO) diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 16d307e2324..8b3c64cebc3 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include #include #include "expr2cpp.h" @@ -321,3 +322,8 @@ void cpp_typecheckt::clean_up() } } } + +bool cpp_typecheckt::builtin_factory(const irep_idt &identifier) +{ + return ::builtin_factory(identifier, symbol_table, get_message_handler()); +} diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h index 29a2a7e0efc..307a6188fa2 100644 --- a/src/cpp/cpp_typecheck.h +++ b/src/cpp/cpp_typecheck.h @@ -346,6 +346,8 @@ class cpp_typecheckt:public c_typecheck_baset _method_symbol, template_map, instantiation_stack)); } + bool builtin_factory(const irep_idt &); + // types void typecheck_type(typet &type); diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index c160b58790e..86fcddea3bc 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -1407,8 +1407,20 @@ exprt cpp_typecheck_resolvet::resolve( qualified?cpp_scopet::QUALIFIED:cpp_scopet::RECURSIVE; if(template_args.is_nil()) + { cpp_typecheck.cpp_scopes.current_scope().lookup( base_name, lookup_kind, id_set); + + if(id_set.empty() && !cpp_typecheck.builtin_factory(base_name)) + { + cpp_idt &builtin_id = + cpp_typecheck.cpp_scopes.get_root_scope().insert(base_name); + builtin_id.identifier = base_name; + builtin_id.id_class = cpp_idt::id_classt::SYMBOL; + + id_set.insert(&builtin_id); + } + } else cpp_typecheck.cpp_scopes.current_scope().lookup( base_name, lookup_kind, cpp_idt::id_classt::TEMPLATE, id_set); From 4edecbc5f46930ee336449c5d877896038bc1485 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 8 Jun 2018 11:42:56 +0000 Subject: [PATCH 8/8] Rename add_cprover_X_library to cprover_X_library_factory This name more clearly describes what these functions do. --- src/ansi-c/cprover_library.cpp | 2 +- src/ansi-c/cprover_library.h | 2 +- src/cbmc/cbmc_parse_options.cpp | 4 ++-- src/cpp/cprover_library.cpp | 2 +- src/cpp/cprover_library.h | 2 +- src/goto-analyzer/goto_analyzer_parse_options.cpp | 5 +++-- src/goto-diff/goto_diff_parse_options.cpp | 6 ++++-- src/goto-instrument/goto_instrument_parse_options.cpp | 6 ++++-- 8 files changed, 17 insertions(+), 12 deletions(-) diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index 895e35809fb..965f0ca823b 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -74,7 +74,7 @@ std::string get_cprover_library_text( return library_text.str(); } -void add_cprover_c_library( +void cprover_c_library_factory( const std::set &functions, symbol_tablet &symbol_table, message_handlert &message_handler) diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h index ed9587cd767..ef0a0f21c34 100644 --- a/src/ansi-c/cprover_library.h +++ b/src/ansi-c/cprover_library.h @@ -32,7 +32,7 @@ void add_library( symbol_tablet &, message_handlert &); -void add_cprover_c_library( +void cprover_c_library_factory( const std::set &functions, symbol_tablet &, message_handlert &); diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e2ab0fac1d5..2df3984c6e4 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -717,9 +717,9 @@ bool cbmc_parse_optionst::process_goto_program( log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom; link_to_library( - goto_model, log.get_message_handler(), add_cprover_cpp_library); + goto_model, log.get_message_handler(), cprover_cpp_library_factory); link_to_library( - goto_model, log.get_message_handler(), add_cprover_c_library); + goto_model, log.get_message_handler(), cprover_c_library_factory); if(options.get_bool_option("string-abstraction")) string_instrumentation(goto_model, log.get_message_handler()); diff --git a/src/cpp/cprover_library.cpp b/src/cpp/cprover_library.cpp index 765f03555ad..fae330e1063 100644 --- a/src/cpp/cprover_library.cpp +++ b/src/cpp/cprover_library.cpp @@ -35,7 +35,7 @@ static std::string get_cprover_library_text( functions, symbol_table, cprover_library, library_text.str()); } -void add_cprover_cpp_library( +void cprover_cpp_library_factory( const std::set &functions, symbol_tablet &symbol_table, message_handlert &message_handler) diff --git a/src/cpp/cprover_library.h b/src/cpp/cprover_library.h index 9c9e76a7fe7..9f08436a2fe 100644 --- a/src/cpp/cprover_library.h +++ b/src/cpp/cprover_library.h @@ -16,7 +16,7 @@ Author: Michael Tautschnig class message_handlert; class symbol_tablet; -void add_cprover_cpp_library( +void cprover_cpp_library_factory( const std::set &functions, symbol_tablet &, message_handlert &); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 3493b8cd9a0..4fd380ed877 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -729,8 +729,9 @@ 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); + link_to_library( + goto_model, ui_message_handler, cprover_cpp_library_factory); + link_to_library(goto_model, ui_message_handler, cprover_c_library_factory); #endif // remove function pointers diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index f8f4b50dc46..a106114cca5 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -398,8 +398,10 @@ 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); + link_to_library( + goto_model, get_message_handler(), cprover_cpp_library_factory); + link_to_library( + goto_model, get_message_handler(), cprover_c_library_factory); // remove function pointers status() << "Removal of function pointers and virtual functions" << eom; diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 1f863c6a2fd..fdb1fc664f6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -961,8 +961,10 @@ 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); + link_to_library( + goto_model, get_message_handler(), cprover_cpp_library_factory); + link_to_library( + goto_model, get_message_handler(), cprover_c_library_factory); } // now do full inlining, if requested