Merge pull request #5285 from thk123/cpp-new-cmake

Fix CPP models when using CMake Build

Author: tautschnig

regression/cbmc-cpp/cpp-new/main.cpp

@@ -0,0 +1,9 @@
+#include <cassert>
+
+int main()
+{
+  int *some_data = new int(10);
+  assert(some_data);
+  assert(*some_data == 10);
+  return 0;
+}

regression/cbmc-cpp/cpp-new/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.cpp
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Ensure that the new operator is implemented.

regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--string-abstraction --show-goto-functions
+strlen#return_value = \(.*\)s#strarg->length - POINTER_OFFSET\(s\);
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure that the --string-abstraction flag enables the string abstraction
+version of string functions

regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--show-goto-functions
+IF !\(\(signed int\)s\[\(.*\)len\] != 0\) THEN GOTO 2
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure that if the string abstraction flag is not provided, the regular model for
+string functions is used (in this case searching for the terminator).

regression/cbmc-library/string-abstraction/test.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  char *x = malloc(sizeof(char) * 10);
+  x[8] = '\0';
+  assert(strlen(x) == 8);
+}

src/ansi-c/cprover_library.cpp

@@ -45,7 +45,9 @@ std::string get_cprover_library_text(
   const struct cprover_library_entryt cprover_library[],
   const std::string &prologue)
 {
-  std::ostringstream library_text(prologue);
+  // the default mode is ios_base::out which means subsequent write to the
+  // stream will overwrite the original content
+  std::ostringstream library_text(prologue, std::ios_base::ate);
 
   std::size_t count=0;
 

src/cpp/CMakeLists.txt

@@ -1,14 +1,8 @@
 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
-)
+        COMMAND cat ${cpp_library_sources} | $<TARGET_FILE:converter> > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
+        DEPENDS converter ${cpp_library_sources})
 
 ################################################################################
 
@@ -33,6 +27,12 @@ endif()
 file(GLOB_RECURSE sources "*.cpp" "*.h")
 add_library(cpp ${sources})
 
+set_source_files_properties(
+        ${sources}
+        PROPERTIES
+        OBJECT_DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
+)
+
 generic_includes(cpp)
 
 target_link_libraries(cpp util ansi-c)