3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

Merge pull request #1138 from delcypher/cmake_serious_warnings

Support serious warnings in CMake and TravisCI
This commit is contained in:
Nikolaj Bjorner 2017-07-14 11:14:35 +02:00 committed by GitHub
commit 8a57e081f7
7 changed files with 124 additions and 9 deletions

View file

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

View file

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

View file

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

View file

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

View file

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

View file

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

View file

@ -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"