diff --git a/.clang-format b/.clang-format index fdd2d857fcd7..6b5af452210e 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 8945f9429c6d..2b239c41e033 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -72,10 +72,9 @@ 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} -std=c++17 -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 + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} /std:c++17 /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF ") # Include Git Bash Environment (rqeuired for download_project (patch)) find_package(Git) @@ -180,16 +179,12 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR endif() function(cprover_default_properties) - 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( ${ARGN} PROPERTIES - CXX_STANDARD ${CBMC_CXX_STANDARD} - CXX_STANDARD_REQUIRED ${CBMC_CXX_STANDARD_REQUIRED} XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY ${CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY}) endfunction() diff --git a/COMPILING.md b/COMPILING.md index 3fb133a1be30..eec73be1c953 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -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 e000b469beac..4f2e79a84faf 100755 --- a/scripts/bash-autocomplete/extract_switches.sh +++ b/scripts/bash-autocomplete/extract_switches.sh @@ -1,6 +1,6 @@ #!/bin/bash echo "Compiling the helper file to extract the raw list of parameters from cbmc" -g++ -c -MMD -MP -std=c++11 -Wall -I ../../src/ -ftrack-macro-expansion=0 -fno-diagnostics-show-caret switch_extractor_helper.c -o tmp.o 2> pragma.txt +g++ -c -MMD -MP -std=c++17 -Wall -I ../../src/ -ftrack-macro-expansion=0 -fno-diagnostics-show-caret switch_extractor_helper.c -o tmp.o 2> pragma.txt retval=$? diff --git a/scripts/glucose_CMakeLists.txt b/scripts/glucose_CMakeLists.txt index b2116ce91f4b..2faee91eeb9b 100644 --- a/scripts/glucose_CMakeLists.txt +++ b/scripts/glucose_CMakeLists.txt @@ -9,8 +9,6 @@ add_library(glucose-condensed set_target_properties( glucose-condensed PROPERTIES - CXX_STANDARD 11 - 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 963bc0a6d1d0..f2b9f580b4b7 100644 --- a/scripts/minisat2_CMakeLists.txt +++ b/scripts/minisat2_CMakeLists.txt @@ -9,8 +9,6 @@ add_library(minisat2-condensed set_target_properties( minisat2-condensed PROPERTIES - CXX_STANDARD 11 - CXX_STANDARD_REQUIRED true XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" ) diff --git a/src/common b/src/common index d6de5219be71..7ddf92fa5e02 100644 --- a/src/common +++ b/src/common @@ -34,11 +34,11 @@ 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++ 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 @@ -102,13 +102,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 @@ -133,7 +133,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 c32196f1c59f..f63d306d2046 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 35228291219c..3bf00199746f 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -1,6 +1,3 @@ -set(CMAKE_CXX_STANDARD 11) -set(CMAKE_CXX_STANDARD_REQUIRED true) - # We may use one of several different solver libraries. # The following files wrap the chosen solver library. # We remove them all from the solver-library sources list, and then add the @@ -109,7 +106,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 +136,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 )