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

CMake doesn't know about C++ 17 until version 3.8, so we need to
hard-code the necessary command-line options.

Author: tautschnig

.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

@@ -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)
@@ -181,16 +180,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()
 

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

scripts/minisat2_CMakeLists.txt

@@ -10,8 +10,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"
 )
 

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
@@ -103,13 +103,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
@@ -134,7 +134,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/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)

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
     )