Merge pull request #4382 from karkhaz/kk-optional-jbmc

Make JBMC build optional with cmake

Author: karkhaz

CMakeLists.txt

@@ -117,7 +117,10 @@ add_subdirectory(src)
 add_subdirectory(regression)
 add_subdirectory(unit)
 
-add_subdirectory(jbmc)
+set(CBMC_CXX_STANDARD 11)
+set(CBMC_CXX_STANDARD_REQUIRED true)
+set(CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY
+    "Developer ID Application: Daniel Kroening")
 
 set_target_properties(
     analyses
@@ -152,20 +155,13 @@ set_target_properties(
     util
     xml
 
-    java_bytecode
-    java-models-library
-    jbmc
-    jbmc-lib
-    janalyzer
-    janalyzer-lib
-    jdiff
-    jdiff-lib
-    java-testing-utils
-    java-unit
-    miniz
-
     PROPERTIES
-    CXX_STANDARD 11
-    CXX_STANDARD_REQUIRED true
-    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
+    CXX_STANDARD ${CBMC_CXX_STANDARD}
+    CXX_STANDARD_REQUIRED ${CBMC_CXX_STANDARD_REQUIRED}
+    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY ${CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY}
 )
+
+option(WITH_JBMC "Build the JBMC Java front-end" ON)
+if(WITH_JBMC)
+    add_subdirectory(jbmc)
+endif()

COMPILING.md

@@ -219,6 +219,9 @@ require manual modification of build files.
      ```
      You shoud also install [Homebrew](https://brew.sh), after which you can
      run `brew install cmake` to install CMake.
+   - On platforms where installing the Java Development Kit and Maven is
+     difficult, you can avoid needing these dependencies by not building
+     JBMC. Just pass `-DWITH_JBMC=OFF` to cmake in step (4) below.
    - On Windows, ensure you have Visual Studio 2015 or later installed.
      Then, download CMake from the [official download
      page](https://cmake.org/download).

jbmc/CMakeLists.txt

@@ -7,3 +7,22 @@ add_custom_target(java-models-library ALL
     COMMAND cp target/core-models.jar ${CMAKE_CURRENT_SOURCE_DIR}/src/java_bytecode/library/
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library
 )
+
+set_target_properties(
+    java_bytecode
+    java-models-library
+    jbmc
+    jbmc-lib
+    janalyzer
+    janalyzer-lib
+    jdiff
+    jdiff-lib
+    java-testing-utils
+    java-unit
+    miniz
+
+    PROPERTIES
+    CXX_STANDARD ${CBMC_CXX_STANDARD}
+    CXX_STANDARD_REQUIRED ${CBMC_CXX_STANDARD_REQUIRED}
+    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY ${CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY}
+)