mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

rename additional build options #2709

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-18 20:50:53 -08:00
parent e9d9792524
commit b50f8508f2
5 changed files with 18 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
CMakeLists.txt
View file

@ -392,12 +392,12 @@ include(${PROJECT_SOURCE_DIR}/cmake/compiler_lto.cmake)
################################################################################ ################################################################################
# Control flow integrity # Control flow integrity
################################################################################ ################################################################################
option(ENABLE_CFI "Enable control flow integrity checking" OFF) option(Z3_ENABLE_CFI "Enable control flow integrity checking" OFF)
if (ENABLE_CFI) if (Z3_ENABLE_CFI)
set(build_types_with_cfi "RELEASE" "RELWITHDEBINFO") set(build_types_with_cfi "RELEASE" "RELWITHDEBINFO")
if (NOT LINK_TIME_OPTIMIZATION) if (NOT Z3_LINK_TIME_OPTIMIZATION)
message(FATAL_ERROR "Cannot enable control flow integrity checking without link-time optimization." message(FATAL_ERROR "Cannot enable control flow integrity checking without link-time optimization."
"You should set LINK_TIME_OPTIMIZATION to ON or ENABLE_CFI to OFF.") "You should set Z3_LINK_TIME_OPTIMIZATION to ON or Z3_ENABLE_CFI to OFF.")
endif() endif()
if (DEFINED CMAKE_CONFIGURATION_TYPES) if (DEFINED CMAKE_CONFIGURATION_TYPES)
# Multi configuration generator # Multi configuration generator
@ -417,7 +417,7 @@ if (ENABLE_CFI)
endforeach() endforeach()
else() else()
message(FATAL_ERROR "Can't enable control flow integrity for compiler \"${CMAKE_CXX_COMPILER_ID}\"." message(FATAL_ERROR "Can't enable control flow integrity for compiler \"${CMAKE_CXX_COMPILER_ID}\"."
"You should set ENABLE_CFI to OFF or use Clang or MSVC to compile.") "You should set Z3_ENABLE_CFI to OFF or use Clang or MSVC to compile.")
endif() endif()
endif() endif()

8
README-CMake.md
View file

@ -261,11 +261,11 @@ The following useful options can be passed to CMake whilst configuring.
* ``Z3_BUILD_DOCUMENTATION`` - BOOL. If set to ``TRUE`` then documentation for the API bindings can be built by invoking the ``api_docs`` target. * ``Z3_BUILD_DOCUMENTATION`` - BOOL. If set to ``TRUE`` then documentation for the API bindings can be built by invoking the ``api_docs`` target.
* ``Z3_INSTALL_API_BINDINGS_DOCUMENTATION`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_DOCUMENTATION` is ``TRUE`` then documentation for API bindings will be installed * ``Z3_INSTALL_API_BINDINGS_DOCUMENTATION`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_DOCUMENTATION` is ``TRUE`` then documentation for API bindings will be installed
when running the ``install`` target. when running the ``install`` target.
* ``ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION`` is ``TRUE`` then documentation for API bindings will always be built. * ``Z3_ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_DOCUMENTATION`` is ``TRUE`` then documentation for API bindings will always be built.
Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target. Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target.
* ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled. * ``Z3_LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled.
* ``ENABLE_CFI`` - BOOL. If set to ``TRUE`` will enable Control Flow Integrity security checks. This is only supported by MSVC and Clang and will * ``Z3_ENABLE_CFI`` - BOOL. If set to ``TRUE`` will enable Control Flow Integrity security checks. This is only supported by MSVC and Clang and will
fail on other compilers. This requires LINK_TIME_OPTIMIZATION to also be enabled. fail on other compilers. This requires Z3_LINK_TIME_OPTIMIZATION to also be enabled.
* ``Z3_API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature. * ``Z3_API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
* ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors. * ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors.
If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors. If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors.

8
cmake/compiler_lto.cmake
View file

@ -1,6 +1,6 @@
option(LINK_TIME_OPTIMIZATION "Use link time optimiziation" OFF) option(Z3_LINK_TIME_OPTIMIZATION "Use link time optimiziation" OFF)
if (LINK_TIME_OPTIMIZATION) if (Z3_LINK_TIME_OPTIMIZATION)
message(STATUS "LTO enabled") message(STATUS "LTO enabled")
set(build_types_with_lto "RELEASE" "RELWITHDEBINFO") set(build_types_with_lto "RELEASE" "RELWITHDEBINFO")
if (DEFINED CMAKE_CONFIGURATION_TYPES) if (DEFINED CMAKE_CONFIGURATION_TYPES)
@ -12,7 +12,7 @@ if (LINK_TIME_OPTIMIZATION)
list(FIND build_types_with_lto "${_build_type_upper}" _index) list(FIND build_types_with_lto "${_build_type_upper}" _index)
if ("${_index}" EQUAL -1) if ("${_index}" EQUAL -1)
message(FATAL_ERROR "Configuration ${CMAKE_BUILD_TYPE} does not support LTO." message(FATAL_ERROR "Configuration ${CMAKE_BUILD_TYPE} does not support LTO."
"You should set LINK_TIME_OPTIMIZATION to OFF.") "You should set Z3_LINK_TIME_OPTIMIZATION to OFF.")
endif() endif()
endif() endif()
@ -27,7 +27,7 @@ if (LINK_TIME_OPTIMIZATION)
set(_lto_linker_flag "/LTCG") set(_lto_linker_flag "/LTCG")
else() else()
message(FATAL_ERROR "Can't enable LTO for compiler \"${CMAKE_CXX_COMPILER_ID}\"." message(FATAL_ERROR "Can't enable LTO for compiler \"${CMAKE_CXX_COMPILER_ID}\"."
"You should set LINK_TIME_OPTIMIZATION to OFF.") "You should set Z3_LINK_TIME_OPTIMIZATION to OFF.")
endif() endif()
CHECK_CXX_COMPILER_FLAG("${_lto_compiler_flag}" HAS_LTO) CHECK_CXX_COMPILER_FLAG("${_lto_compiler_flag}" HAS_LTO)
if (NOT HAS_LTO) if (NOT HAS_LTO)

4
contrib/ci/scripts/build_z3_cmake.sh
View file

@ -41,9 +41,9 @@ fi
# Use link time optimziation? # Use link time optimziation?
if [ "X${USE_LTO}" = "X1" ]; then if [ "X${USE_LTO}" = "X1" ]; then
ADDITIONAL_Z3_OPTS+=('-DLINK_TIME_OPTIMIZATION=ON') ADDITIONAL_Z3_OPTS+=('-DZ3_LINK_TIME_OPTIMIZATION=ON')
else else
ADDITIONAL_Z3_OPTS+=('-DLINK_TIME_OPTIMIZATION=OFF') ADDITIONAL_Z3_OPTS+=('-DZ3_LINK_TIME_OPTIMIZATION=OFF')
fi fi
# Build API docs? # Build API docs?

6
doc/CMakeLists.txt
View file

@ -41,8 +41,8 @@ else()
list(APPEND JAVA_API_OPTIONS "--no-java") list(APPEND JAVA_API_OPTIONS "--no-java")
endif() endif()
option(ALWAYS_BUILD_DOCS "Always build documentation for API bindings" ON) option(Z3_ALWAYS_BUILD_DOCS "Always build documentation for API bindings" ON)
if (ALWAYS_BUILD_DOCS) if (Z3_ALWAYS_BUILD_DOCS)
set(ALWAYS_BUILD_DOCS_ARG "ALL") set(ALWAYS_BUILD_DOCS_ARG "ALL")
else() else()
set(ALWAYS_BUILD_DOCS_ARG "") set(ALWAYS_BUILD_DOCS_ARG "")
@ -51,7 +51,7 @@ else()
message(WARNING "Building documentation for API bindings is not part of the" message(WARNING "Building documentation for API bindings is not part of the"
" all target. This may result in stale files being installed when running" " all target. This may result in stale files being installed when running"
" the install target. You should run the api_docs target before running" " the install target. You should run the api_docs target before running"
" the install target. Alternatively Set ALWAYS_BUILD_DOCS to ON to" " the install target. Alternatively Set Z3_ALWAYS_BUILD_DOCS to ON to"
" automatically build documentation when running the install target." " automatically build documentation when running the install target."
) )
endif() endif()