Set the correct C++ standard version so that regression test pass rel…

[martin-cs]

…iably

This should address issue:

#6090

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[tautschnig]

We might actually need to use our understanding of the underlying GCC version and set the default accordingly.

[martin-cs]

@tautschnig That would likely be a better option; this is a work around.

[tautschnig]

I'd propose the following patch instead, which should likely be turned into several commits (adding some handling of C++17 and then making the compiler defaults visible via the changes in configure_gcc):

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index f2d3043e43..962a29e5ec 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -814,7 +814,8 @@ void goto_checkt::integer_overflow_check(
       {
         if(
           config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
-          config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14)
+          config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14 ||
+          config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17)
         {
           allow_shift_into_sign_bit = false;
         }
diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp
index 0c3b76dab6..03f6d5d58d 100644
--- a/src/ansi-c/c_preprocess.cpp
+++ b/src/ansi-c/c_preprocess.cpp
@@ -551,6 +551,15 @@ bool c_preprocess_gcc_clang(
 #endif
         argv.push_back("-std=gnu++14");
       break;
+
+    case configt::cppt::cpp_standardt::CPP17:
+#if defined(__OpenBSD__)
+      if(preprocessor == configt::ansi_ct::preprocessort::CLANG)
+        argv.push_back("-std=c++17");
+      else
+#endif
+        argv.push_back("-std=gnu++17");
+      break;
     }
   }
   else
diff --git a/src/ansi-c/gcc_version.cpp b/src/ansi-c/gcc_version.cpp
index b23b69ea91..e4fb06e9ad 100644
--- a/src/ansi-c/gcc_version.cpp
+++ b/src/ansi-c/gcc_version.cpp
@@ -120,6 +120,8 @@ void gcc_versiont::get(const std::string &executable)
               default_cxx_standard = configt::cppt::cpp_standardt::CPP11;
             else if(split[1] == "201402L")
               default_cxx_standard = configt::cppt::cpp_standardt::CPP14;
+            else if(split[1] == "201703L")
+              default_cxx_standard = configt::cppt::cpp_standardt::CPP17;
           }
         }
       }
@@ -160,4 +162,7 @@ void configure_gcc(const gcc_versiont &gcc_version)
   config.ansi_c.gcc__float128_type =
     gcc_version.flavor == gcc_versiont::flavort::GCC &&
     gcc_version.is_at_least(4u, gcc_float128_minor_version);
+
+  config.ansi_c.c_standard = gcc_version.default_c_standard;
+  config.cpp.cpp_standard = gcc_version.default_cxx_standard;
 }
diff --git a/src/cpp/cpp_parser.cpp b/src/cpp/cpp_parser.cpp
index e73fba627f..74e861286a 100644
--- a/src/cpp/cpp_parser.cpp
+++ b/src/cpp/cpp_parser.cpp
@@ -21,9 +21,10 @@ bool cpp_parsert::parse()
 {
   // We use the ANSI-C scanner
   ansi_c_parser.cpp98=true;
-  ansi_c_parser.cpp11=
-    config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP11 ||
-    config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP14;
+  ansi_c_parser.cpp11 =
+    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
+    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14 ||
+    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17;
   ansi_c_parser.ts_18661_3_Floatn_types=false;
   ansi_c_parser.in=in;
   ansi_c_parser.mode=mode;
diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
index 5cfc38998c..4b2280fb3a 100644
--- a/src/goto-cc/gcc_mode.cpp
+++ b/src/goto-cc/gcc_mode.cpp
@@ -593,6 +593,9 @@ int gcc_modet::doit()

     if(std_string=="gnu++14" || std_string=="c++14")
       config.cpp.set_cpp14();
+
+    if(std_string == "gnu++17" || std_string == "c++17")
+      config.cpp.set_cpp17();
   }
   else
   {
diff --git a/src/util/config.h b/src/util/config.h
index 9ec75d2886..bfeb8c8555 100644
--- a/src/util/config.h
+++ b/src/util/config.h
@@ -231,6 +231,10 @@ public:
     void set_cpp03() { cpp_standard=cpp_standardt::CPP03; }
     void set_cpp11() { cpp_standard=cpp_standardt::CPP11; }
     void set_cpp14() { cpp_standard=cpp_standardt::CPP14; }
+    void set_cpp17()
+    {
+      cpp_standard = cpp_standardt::CPP17;
+    }

     static const std::size_t default_object_bits=8;
   } cpp;

[lzaoral]

Hi!
I'm a new co-maintainer of the cbmc package in Fedora. Nice to meet you all!

I've tried the patch proposed by @tautschnig and I had to add the following change for a successful compilation:

--- a/src/util/config.h
+++ b/src/util/config.h
@@ -224,7 +224,7 @@
   struct cppt
   {
-    enum class cpp_standardt { CPP98, CPP03, CPP11, CPP14 } cpp_standard;
+    enum class cpp_standardt { CPP98, CPP03, CPP11, CPP14, CPP17 } cpp_standard;
     static cpp_standardt default_cpp_standard();
 
     void set_cpp98() { cpp_standard=cpp_standardt::CPP98; }

I can confirm that it fixes this particular issue. However, it uncovered a couple of other issues and resulted in a few test failures (see the build log). I see that one of them was already reported last year by a former maintainer as #5337.

[martin-cs]

@lzaoral This is getting a little confusing. Please could you submit a PR with the version of @tautschnig 's code that you used. Please tag #5337 and #6090 and then we can close this PR and just focus on your PR to resolve those two issues. It will be easier when we can see the diff and the CI results.

[martin-cs]

Closed in favour of #6402