Aggregating all library dependencies into one

CBMC is compiled as a collection of static libraries, one per
sub-module.  This commits add a merging of most submodules into a final
libcprover.<version>.a, so that it can be installed and used alone (without
requiring its sub-module dependencies).

Author: Enrico Steffinlongo

src/CMakeLists.txt

@@ -110,7 +110,6 @@ add_subdirectory(jsil)
 add_subdirectory(json)
 add_subdirectory(json-symtab-language)
 add_subdirectory(langapi)
-add_subdirectory(libcprover-cpp)
 add_subdirectory(linking)
 add_subdirectory(pointer-analysis)
 add_subdirectory(solvers)
@@ -127,6 +126,7 @@ add_subdirectory(goto-diff)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-synthesizer)
 add_subdirectory(symtab2gb)
+add_subdirectory(libcprover-cpp)
 
 if(UNIX OR WITH_MEMORY_ANALYZER)
 add_subdirectory(memory-analyzer)

src/libcprover-cpp/CMakeLists.txt

@@ -1,23 +1,70 @@
-file(GLOB_RECURSE sources "*.cpp" "*.h")
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
 
-# This step builds the API in the form of a statically linked library (libcprover-api-cpp.a)
+# This step builds the API in the form of a statically linked library
 add_library(cprover-api-cpp ${sources})
+
+# Being a library we should include them privately, but for now fair enough
 generic_includes(cprover-api-cpp)
-target_link_libraries(cprover-api-cpp 
-    goto-checker
-    goto-programs
-    util
-    langapi
-    ansi-c
-    json-symtab-language
-    solvers
-    xml
-    cpp
-    cbmc-lib
-    analyses
-    statement-list
-    linking
-    pointer-analysis
-    goto-instrument-lib
-    goto-analyzer-lib
-    goto-cc-lib)
+
+target_include_directories(cprover-api-cpp PUBLIC
+                           "$<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>"
+                           "$<BUILD_INTERFACE:${CMAKE_CURRENT_BINARY_DIR}>"
+                           "$<INSTALL_INTERFACE:include>")
+
+get_target_property(LIBRARY_DEPENDENCIES solvers LINK_LIBRARIES)
+
+list(APPEND
+        LIBRARY_DEPENDENCIES
+        "goto-programs"
+        "util"
+        "langapi"
+        "ansi-c"
+        "analyses"
+        "goto-instrument-lib"
+        "big-int"
+        "linking"
+        "goto-checker"
+        "solvers"
+        "assembler"
+        "xml"
+        "json"
+        "json-symtab-language"
+        "jsil"
+        "statement-list"
+        "goto-symex"
+        "pointer-analysis"
+        "cbmc-lib")
+
+list(REMOVE_DUPLICATES LIBRARY_DEPENDENCIES)
+
+target_link_libraries(cprover-api-cpp
+                      PRIVATE
+                      ${LIBRARY_DEPENDENCIES})
+
+set(DEPENDENCY_TARGETS "")
+foreach(dep ${LIBRARY_DEPENDENCIES})
+    list(APPEND DEPENDENCY_TARGETS "$<TARGET_FILE:${dep}>")
+endforeach(dep LIBRARY_DEPENDENCIES)
+
+string(REPLACE ";" " " DEPENDENCY_TARGETS "${DEPENDENCY_TARGETS}")
+
+add_custom_command(TARGET cprover-api-cpp POST_BUILD
+                   COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/add_dependencies.sh" "${CMAKE_AR}" "$<TARGET_FILE:cprover-api-cpp>" "${DEPENDENCY_TARGETS}"
+                   WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}")
+
+set_target_properties(cprover-api-cpp
+        PROPERTIES
+        OUTPUT_NAME "cprover.${CMAKE_PROJECT_VERSION}" # libcprover.<version>.a
+        SOVERSION "${CMAKE_PROJECT_VERSION}"
+        PUBLIC_HEADER "${headers}"
+        )
+
+install(TARGETS         cprover-api-cpp
+        ARCHIVE         DESTINATION "${CMAKE_INSTALL_LIBDIR}"
+                        COMPONENT lib
+        LIBRARY         DESTINATION "${CMAKE_INSTALL_LIBDIR}"
+                        COMPONENT lib
+        PUBLIC_HEADER   DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/cprover"
+                        COMPONENT lib
+        )

src/libcprover-cpp/add_dependencies.sh

@@ -0,0 +1,15 @@
+#!/usr/bin/env sh
+
+set -e
+
+AR_COMMAND=$1
+shift
+DESTINATION=$1
+shift
+LIB_LIST=$@
+
+for lib in ${LIB_LIST}; do
+  ${AR_COMMAND} -x ${lib}
+done
+
+${AR_COMMAND} -rcs ${DESTINATION} *.o