Merge pull request #7989 from esteffin/esteffin/cpp-17

Change C++ version to C++17

Author: Enrico Steffinlongo

.clang-format

@@ -71,7 +71,7 @@ SpacesInCStyleCastParentheses: 'false'
 SpacesInContainerLiterals: 'false'
 SpacesInParentheses: 'false'
 SpacesInSquareBrackets: 'false'
-Standard: c++11
+Standard: c++17
 TabWidth: '2'
 UseTab: Never
 ---

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

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:
    ```

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"

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

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)\""

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

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

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:$@ $^

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