Make JBMC build optional with cmake

This commit adds an option to CMake, `WITH_JBMC`, that controls whether
the jbmc directory will be built. It is switched on by default,
preserving the current behaviour.

The motivation is to make it as easy as possible for users to get
started with CBMC, especially users who are only interested in the C
front-end and are on Windows, where installing the JDK and Maven is a
painful exercise.

Also updated `COMPILING.md` to note that you can pass `-DWITH_JBMC=OFF`
to cmake to avoid building jbmc.
This commit is contained in:
Kareem Khazem 2019-03-13 16:02:22 -07:00
parent 2c63234cd1
commit 562fad22ee
No known key found for this signature in database
GPG Key ID: 3A0F7E9F63800E38
3 changed files with 34 additions and 16 deletions

View File

@ -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()

View File

@ -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).

View File

@ -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}
)