From 9f2d2093226de8878183ab369ff73ba00e8b473e Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Mon, 30 Oct 2023 16:30:18 +0000 Subject: [PATCH 1/4] Switch cmake build to c++17 Changing the C++ standard to C++ 17 on the cmake-based build-system. --- CMakeLists.txt | 9 +++++++-- scripts/cadical_CMakeLists.txt | 3 ++- scripts/glucose_CMakeLists.txt | 3 ++- scripts/minisat2_CMakeLists.txt | 3 ++- src/solvers/CMakeLists.txt | 3 --- 5 files changed, 13 insertions(+), 8 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index bed1ee334b5..a64f6778bbb 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,5 +1,9 @@ cmake_minimum_required(VERSION 3.8) +set(CMAKE_CXX_STANDARD 17) +set(CMAKE_CXX_STANDARD_REQUIRED true) +set(CMAKE_CXX_EXTENSIONS OFF) + # Compile with /usr/bin/clang on MacOS # See https://github.com/diffblue/cbmc/issues/4956 # @@ -186,8 +190,9 @@ 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_CXX_STANDARD ${CMAKE_CXX_STANDARD}) + set(CBMC_CXX_STANDARD_REQUIRED ${CMAKE_CXX_STANDARD_REQUIRED}) + set(CBMC_CXX_EXTENSIONS ${CMAKE_CXX_EXTENSIONS}) set(CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening") diff --git a/scripts/cadical_CMakeLists.txt b/scripts/cadical_CMakeLists.txt index 0ef36e66e3a..9dcb6d27230 100644 --- a/scripts/cadical_CMakeLists.txt +++ b/scripts/cadical_CMakeLists.txt @@ -14,8 +14,9 @@ target_compile_options(cadical PUBLIC -DNBUILD) set_target_properties( cadical PROPERTIES - CXX_STANDARD 11 + CXX_STANDARD 17 CXX_STANDARD_REQUIRED true + CXX_EXTENSIONS OFF XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" ) diff --git a/scripts/glucose_CMakeLists.txt b/scripts/glucose_CMakeLists.txt index b2116ce91f4..55014a6d30f 100644 --- a/scripts/glucose_CMakeLists.txt +++ b/scripts/glucose_CMakeLists.txt @@ -9,8 +9,9 @@ add_library(glucose-condensed set_target_properties( glucose-condensed PROPERTIES - CXX_STANDARD 11 + CXX_STANDARD 17 CXX_STANDARD_REQUIRED true + CXX_EXTENSIONS OFF XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" ) diff --git a/scripts/minisat2_CMakeLists.txt b/scripts/minisat2_CMakeLists.txt index 71e39ff35b4..c6e448a122e 100644 --- a/scripts/minisat2_CMakeLists.txt +++ b/scripts/minisat2_CMakeLists.txt @@ -10,8 +10,9 @@ add_library(minisat2-condensed set_target_properties( minisat2-condensed PROPERTIES - CXX_STANDARD 11 + CXX_STANDARD 17 CXX_STANDARD_REQUIRED true + CXX_EXTENSIONS OFF XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" ) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index daa0853a573..14d00cb94ee 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 From dff50eb33191c4e9a0057c5b9dcaeaaac2e6fc6e Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Mon, 30 Oct 2023 17:00:15 +0000 Subject: [PATCH 2/4] Switch gnu make build to c++17 Changing the C++ standard to C++ 17 on the gnu-make-based build-system --- scripts/bash-autocomplete/extract_switches.sh | 2 +- scripts/check_help.sh | 2 +- src/common | 12 ++++++------ 3 files changed, 8 insertions(+), 8 deletions(-) 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/src/common b/src/common index ff324aaeca2..a3dc18db5fb 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) $(HOSTLINKFLAGS) -std=c++11 -o $@ $^ -static + LINKNATIVE = $(HOSTCXX) $(HOSTLINKFLAGS) -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:$@ $^ From f3c7efe0d984eb7b06caf92ec5edda20dcc7e45b Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 31 Oct 2023 16:23:31 +0000 Subject: [PATCH 3/4] Switch clang-format style to c++17 --- .clang-format | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 --- From 032f68cf8793bd3695a6d3396bbac2f8424af1c4 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 31 Oct 2023 16:24:39 +0000 Subject: [PATCH 4/4] Changed COMPILING.md to use c++17 Changing the documentation COMPILING.md to reflect the change to C++17. Also increased the minimum G++ version to 7 as it is the lowest version with full C++17 support. --- COMPILING.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/COMPILING.md b/COMPILING.md index 80a754dba8c..191f4cddd6a 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: ```