diff --git a/README-CMake.md b/README-CMake.md index 7550808fc..715cacad2 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -266,6 +266,8 @@ The following useful options can be passed to CMake whilst configuring. 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. * ``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. + If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. @@ -381,3 +383,13 @@ It is tempting use file-globbing in ``CMakeLists.txt`` to find a set for files m use them as the sources to build a target. This however is a bad idea because it prevents CMake from knowing when it needs to rerun itself. This is why source file names are explicitly listed in the ``CMakeLists.txt`` so that when changes are made the source files used to build a target automatically triggers a rerun of CMake. Long story short. Don't use file globbing. + +### Serious warning flags + +By default the `WARNINGS_AS_ERRORS` flag is set to `SERIOUS_ONLY` which means +some warnings will be treated as errors. These warnings are controlled by the +relevant `*_WARNINGS_AS_ERRORS` list defined in +`cmake/compiler_warnings.cmake`. + +Additional warnings should only be added here if the warnings has no false +positives. diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index e02b28b2c..183f490dd 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -1,17 +1,61 @@ +################################################################################ +# Compiler warning flags +################################################################################ +# These are passed to relevant compiler provided they are supported set(GCC_AND_CLANG_WARNINGS - "-Wall" + "-Wall" ) set(GCC_ONLY_WARNINGS "") set(CLANG_ONLY_WARNINGS "") set(MSVC_WARNINGS "/W3") +################################################################################ +# Serious warnings +################################################################################ +# This declares the flags that are passed to the compiler when +# `WARNINGS_AS_ERRORS` is set to `SERIOUS_ONLY`. Only flags that are supported +# by the compiler are used. +# +# In effect this a "whitelist" approach where we explicitly tell the compiler +# which warnings we want to be treated as errors. The alternative would be a +# "blacklist" approach where we ask the compiler to treat all warnings are +# treated as errors but then we explicitly list which warnings which should be +# allowed. +# +# The "whitelist" approach seems simpiler because we can incrementally add +# warnings we "think are serious". + +# TODO: Add more warnings that are considered serious enough that we should +# treat them as errors. +set(GCC_AND_CLANG_WARNINGS_AS_ERRORS + # https://clang.llvm.org/docs/DiagnosticsReference.html#wodr + "-Werror=odr" +) +set(GCC_WARNINGS_AS_ERRORS + "" +) +set(CLANG_WARNINGS_AS_ERRORS + # https://clang.llvm.org/docs/DiagnosticsReference.html#wdelete-non-virtual-dtor + "-Werror=delete-non-virtual-dtor" + # https://clang.llvm.org/docs/DiagnosticsReference.html#woverloaded-virtual + "-Werror=overloaded-virtual" +) + +################################################################################ +# Test warning/error flags +################################################################################ set(WARNING_FLAGS_TO_CHECK "") +set(WARNING_AS_ERROR_FLAGS_TO_CHECK "") if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_WARNINGS_AS_ERRORS}) elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${CLANG_WARNINGS_AS_ERRORS}) # FIXME: Remove "x.." when CMP0054 is set to NEW elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS}) @@ -31,8 +75,40 @@ foreach (flag ${WARNING_FLAGS_TO_CHECK}) z3_add_cxx_flag("${flag}") endforeach() -option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF) -if (WARNINGS_AS_ERRORS) +# TODO: Remove this eventually. +# Detect legacy `WARNINGS_AS_ERRORS` boolean option and covert to new +# to new option type. +get_property( + WARNINGS_AS_ERRORS_CACHE_VAR_TYPE + CACHE + WARNINGS_AS_ERRORS + PROPERTY + TYPE +) +if ("${WARNINGS_AS_ERRORS_CACHE_VAR_TYPE}" STREQUAL "BOOL") + message(WARNING "Detected legacy WARNINGS_AS_ERRORS option. Upgrading") + set(WARNINGS_AS_ERRORS_DEFAULT "${WARNINGS_AS_ERRORS}") + # Delete old entry + unset(WARNINGS_AS_ERRORS CACHE) +else() + set(WARNINGS_AS_ERRORS_DEFAULT "SERIOUS_ONLY") +endif() + +set(WARNINGS_AS_ERRORS + ${WARNINGS_AS_ERRORS_DEFAULT} + CACHE STRING + "Treat warnings as errors. ON, OFF, or SERIOUS_ONLY" +) + # Set GUI options +set_property( + CACHE + WARNINGS_AS_ERRORS + PROPERTY STRINGS + "ON;OFF;SERIOUS_ONLY" +) + +if ("${WARNINGS_AS_ERRORS}" STREQUAL "ON") + message(STATUS "Treating compiler warnings as errors") if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror") # FIXME: Remove "x.." when CMP0054 is set to NEW @@ -41,8 +117,14 @@ if (WARNINGS_AS_ERRORS) else() message(AUTHOR_WARNING "Unknown compiler") endif() - message(STATUS "Treating compiler warnings as errors") -else() +elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "SERIOUS_ONLY") + message(STATUS "Treating only serious compiler warnings as errors") + # Loop through the flags + foreach (flag ${WARNING_AS_ERROR_FLAGS_TO_CHECK}) + # Add globally because some flags need to be passed at link time. + z3_add_cxx_flag("${flag}" GLOBAL) + endforeach() +elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "OFF") message(STATUS "Not treating compiler warnings as errors") # FIXME: Remove "x.." when CMP0054 is set to NEW if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") @@ -51,4 +133,8 @@ else() # build system. list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX-") endif() +else() + message(FATAL_ERROR + "WARNINGS_AS_ERRORS set to unsupported value \"${WARNINGS_AS_ERRORS}\"" + ) endif() diff --git a/cmake/z3_add_cxx_flag.cmake b/cmake/z3_add_cxx_flag.cmake index 6e756d3b9..d2624d890 100644 --- a/cmake/z3_add_cxx_flag.cmake +++ b/cmake/z3_add_cxx_flag.cmake @@ -2,7 +2,7 @@ include(CheckCXXCompilerFlag) include(CMakeParseArguments) function(z3_add_cxx_flag flag) - CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED" "" "" ${ARGN}) + CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED;GLOBAL" "" "" ${ARGN}) string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}") string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") @@ -16,8 +16,13 @@ function(z3_add_cxx_flag flag) endif() if (HAS_${SANITIZED_FLAG_NAME}) message(STATUS "C++ compiler supports ${flag}") - list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}") - set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE) + if (z3_add_flag_GLOBAL) + # Set globally + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag} " PARENT_SCOPE) + else() + list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}") + set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE) + endif() else() message(STATUS "C++ compiler does not support ${flag}") endif() diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile index 8b922edff..2d16d5394 100644 --- a/contrib/ci/Dockerfiles/z3_build.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -28,6 +28,7 @@ ARG Z3_INSTALL_PREFIX=/usr ARG Z3_STATIC_BUILD=0 # Blank default indicates use latest. ARG Z3_SYSTEM_TEST_GIT_REVISION +ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY ARG Z3_VERBOSE_BUILD_OUTPUT=0 ENV \ @@ -55,6 +56,7 @@ ENV \ Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \ Z3_SYSTEM_TEST_DIR=/home/user/z3_system_test \ Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION} \ + Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \ Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} # We add context across incrementally to maximal cache reuse diff --git a/contrib/ci/README.md b/contrib/ci/README.md index 31bb504b6..2e117c8b1 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -43,6 +43,7 @@ the future. * `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`) * `Z3_STATIC_BUILD` - Build Z3 binaries and libraries statically (`0` or `1`) * `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used. +* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option pased to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`) ### Linux diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh index 98a9724c7..76fd0fb84 100755 --- a/contrib/ci/scripts/build_z3_cmake.sh +++ b/contrib/ci/scripts/build_z3_cmake.sh @@ -20,7 +20,8 @@ set -o pipefail : ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} : ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"} : ${USE_LTO?"USE_LTO must be specified"} -: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX"} +: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"} +: ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"} ADDITIONAL_Z3_OPTS=() @@ -120,6 +121,7 @@ cmake \ -DCMAKE_BUILD_TYPE=${Z3_BUILD_TYPE} \ -DPYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \ -DCMAKE_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} \ + -DWARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \ "${ADDITIONAL_Z3_OPTS[@]}" \ "${Z3_SRC_DIR}" diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh index 21b97788f..84b2dd400 100755 --- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -120,6 +120,13 @@ if [ -n "${NO_SUPPRESS_OUTPUT}" ]; then ) fi +if [ -n "${Z3_WARNINGS_AS_ERRORS}" ]; then + BUILD_OPTS+=( \ + "--build-arg" \ + "Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS}" \ + ) +fi + case ${LINUX_BASE} in ubuntu_14.04) BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_14.04.Dockerfile"