From 0a3b0efd668e854418b40e4de51695f7f0f67178 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Mar 2022 11:37:38 +0000 Subject: [PATCH] Build using C++17 This raises the minimum GCC version supported to 7 (see https://gcc.gnu.org/projects/cxx-status.html#cxx17). Add -Wno-register to silence warnings about the use of the `register` storage class by older flex versions (as present on macOS). --- .clang-format | 2 +- CMakeLists.txt | 4 ++-- COMPILING.md | 4 ++-- scripts/bash-autocomplete/extract_switches.sh | 2 +- scripts/check_help.sh | 2 +- scripts/glucose_CMakeLists.txt | 2 +- scripts/minisat2_CMakeLists.txt | 2 +- src/common | 12 ++++++------ src/config.inc | 2 +- src/solvers/CMakeLists.txt | 6 +++--- 10 files changed, 19 insertions(+), 19 deletions(-) diff --git a/.clang-format b/.clang-format index fdd2d857fcd..6b5af452210 100644 --- a/.clang-format +++ b/.clang-format @@ -71,7 +71,7 @@ SpacesInCStyleCastParentheses: 'false' SpacesInContainerLiterals: 'false' SpacesInParentheses: 'false' SpacesInSquareBrackets: 'false' -Standard: c++11 +Standard: c++17 TabWidth: '2' UseTab: Never --- diff --git a/CMakeLists.txt b/CMakeLists.txt index 38807e9c5c2..e0d705c4114 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -72,7 +72,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR set(CMAKE_CXX_FLAGS_RELEASE "-O2") set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g") # Enable lots of warnings - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wno-register -Wswitch-enum") elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") # This would be the place to enable warnings for Windows builds, although # config.inc doesn't seem to do that currently @@ -181,7 +181,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR endif() function(cprover_default_properties) - set(CBMC_CXX_STANDARD 11) + set(CBMC_CXX_STANDARD 17) set(CBMC_CXX_STANDARD_REQUIRED true) set(CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening") diff --git a/COMPILING.md b/COMPILING.md index 3fb133a1be3..1a186a9081b 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -1,6 +1,6 @@ # What architecture? -CPROVER now needs a C++11 compliant compiler and is known to work in the +CPROVER now needs a C++17 compliant compiler and is known to work in the following environments: - Linux @@ -152,7 +152,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. ``` dnf install gcc gcc-c++ flex bison curl patch ``` - Note that you need g++ version 5.0 or newer. + Note that you need g++ version 7.0 or newer. On Amazon Linux and similar distributions, do as root: ``` diff --git a/scripts/bash-autocomplete/extract_switches.sh b/scripts/bash-autocomplete/extract_switches.sh index c876e420af7..06a480fa925 100755 --- a/scripts/bash-autocomplete/extract_switches.sh +++ b/scripts/bash-autocomplete/extract_switches.sh @@ -6,7 +6,7 @@ set -e cd `dirname $0` echo "Compiling the helper file to extract the raw list of parameters from cbmc" -g++ -E -dM -std=c++11 -I../../src ../../src/cbmc/cbmc_parse_options.cpp -o macros.c +g++ -E -dM -std=c++17 -I../../src ../../src/cbmc/cbmc_parse_options.cpp -o macros.c echo CBMC_OPTIONS >> macros.c echo "Converting the raw parameter list to the format required by autocomplete scripts" diff --git a/scripts/check_help.sh b/scripts/check_help.sh index 67243676693..f524c0fb5d7 100755 --- a/scripts/check_help.sh +++ b/scripts/check_help.sh @@ -33,7 +33,7 @@ for t in \ tool_name=$(basename $t) opt_name=$(echo $tool_name | tr 'a-z-' 'A-Z_') echo "Extracting the raw list of parameters from $tool_name" - g++ -E -dM -std=c++11 -I../src -I../jbmc/src $t/*_parse_options.cpp -o macros.c + g++ -E -dM -std=c++17 -I../src -I../jbmc/src $t/*_parse_options.cpp -o macros.c # goto-analyzer partly uses the spelling "analyser" within the code base echo ${opt_name}_OPTIONS | sed 's/GOTO_ANALYZER/GOTO_ANALYSER/' >> macros.c rawstring="`gcc -E -P -w macros.c` \"?h(help)\"" diff --git a/scripts/glucose_CMakeLists.txt b/scripts/glucose_CMakeLists.txt index b2116ce91f4..918537b2c99 100644 --- a/scripts/glucose_CMakeLists.txt +++ b/scripts/glucose_CMakeLists.txt @@ -9,7 +9,7 @@ add_library(glucose-condensed set_target_properties( glucose-condensed PROPERTIES - CXX_STANDARD 11 + CXX_STANDARD 17 CXX_STANDARD_REQUIRED true XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" ) diff --git a/scripts/minisat2_CMakeLists.txt b/scripts/minisat2_CMakeLists.txt index 71e39ff35b4..89197cd30a9 100644 --- a/scripts/minisat2_CMakeLists.txt +++ b/scripts/minisat2_CMakeLists.txt @@ -10,7 +10,7 @@ add_library(minisat2-condensed set_target_properties( minisat2-condensed PROPERTIES - CXX_STANDARD 11 + CXX_STANDARD 17 CXX_STANDARD_REQUIRED true XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" ) diff --git a/src/common b/src/common index 024ae53b349..bbed799db7a 100644 --- a/src/common +++ b/src/common @@ -34,12 +34,12 @@ endif CP_CFLAGS = -MMD -MP CXXFLAGS ?= -Wall -O2 ifeq ($(filter-out OSX OSX_Universal,$(BUILD_ENV_)),) - CP_CXXFLAGS += -MMD -MP -mmacosx-version-min=10.15 -std=c++11 -stdlib=libc++ + CP_CXXFLAGS += -MMD -MP -mmacosx-version-min=10.15 -std=c++17 -stdlib=libc++ CP_CFLAGS += -mmacosx-version-min=10.15 LINKFLAGS += -mmacosx-version-min=10.15 -stdlib=libc++ LINKNATIVE += -mmacosx-version-min=10.15 -stdlib=libc++ else - CP_CXXFLAGS += -MMD -MP -std=c++11 + CP_CXXFLAGS += -MMD -MP -std=c++17 endif ifeq ($(filter -O%,$(CXXFLAGS)),) CP_CXXFLAGS += -O2 @@ -105,13 +105,13 @@ else ifeq ($(BUILD_ENV_),Cygwin) CFLAGS ?= -Wall -O2 CXXFLAGS ?= -Wall -O2 CP_CFLAGS = -MMD -MP - CP_CXXFLAGS += -MMD -MP -std=c++11 -U__STRICT_ANSI__ + CP_CXXFLAGS += -MMD -MP -std=c++17 -U__STRICT_ANSI__ # Cygwin-g++ has problems with statically linking exception code. # If linking fails, remove -static. - LINKFLAGS = -static -std=c++11 + LINKFLAGS = -static -std=c++17 LINKLIB = ar rcT $@ $^ LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) - LINKNATIVE = $(HOSTCXX) -std=c++11 -o $@ $^ -static + LINKNATIVE = $(HOSTCXX) -std=c++17 -o $@ $^ -static ifeq ($(origin CC),default) #CC = gcc CC = x86_64-w64-mingw32-gcc @@ -136,7 +136,7 @@ else ifeq ($(BUILD_ENV_),MSVC) DEPEXT = .dep EXEEXT = .exe CFLAGS ?= /W3 /O2 /GF - CXXFLAGS ?= /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF + CXXFLAGS ?= /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF /std:c++17 CP_CFLAGS = CP_CXXFLAGS += LINKLIB = lib /NOLOGO /OUT:$@ $^ diff --git a/src/config.inc b/src/config.inc index 408903df7ea..dd44ad52feb 100644 --- a/src/config.inc +++ b/src/config.inc @@ -5,7 +5,7 @@ BUILD_ENV = AUTO ifeq ($(BUILD_ENV),MSVC) #CXXFLAGS += /Wall /WX else - CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations -Wswitch-enum + CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations -Wno-register -Wswitch-enum endif ifeq ($(CPROVER_WITH_PROFILING),1) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 744def4861b..28b0ffcc2ce 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -1,4 +1,4 @@ -set(CMAKE_CXX_STANDARD 11) +set(CMAKE_CXX_STANDARD 17) set(CMAKE_CXX_STANDARD_REQUIRED true) # We may use one of several different solver libraries. @@ -109,7 +109,7 @@ elseif("${sat_impl}" STREQUAL "cadical") download_project(PROJ cadical URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz PATCH_COMMAND true - COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14 + COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++17 URL_MD5 b44874501a175106424f4bd5de29aa59 ) @@ -139,7 +139,7 @@ elseif("${sat_impl}" STREQUAL "ipasir-cadical") download_project(PROJ cadical URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz PATCH_COMMAND true - COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14 + COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++17 URL_MD5 b44874501a175106424f4bd5de29aa59 )