cbmc: recognise -std={c,gnu}++17 options

CBMC will be able to understand code that is compiled with -std=c++17 or
-std=gnu++17.  Otherwise, it fell back to C++03 making the code un-parsable.

Fixes: #6090

Co-authored-by: Michael Tautschnig <[email protected]>
Co-authored-by: Lukas Zaoral <[email protected]>

Author: lzaoral

src/analyses/goto_check.cpp

@@ -834,7 +834,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;
         }

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

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;
           }
         }
       }

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;

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
   {

src/util/config.h

@@ -224,13 +224,14 @@ class configt
 
   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; }
     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;