C/C++ frontends: select standard using the same rules as the compiler we emulate

.travis.yml

@@ -103,7 +103,9 @@ jobs:
             - parallel
             - libc6-dev-i386
       before_install:
-        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+        - mkdir bin
+        - ln -s /usr/bin/gcc-5 bin/gcc
+        - ln -s /usr/bin/g++-5 bin/g++
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env:
         - COMPILER="ccache /usr/bin/g++-5"
@@ -136,7 +138,9 @@ jobs:
             - libubsan0
             - libc6-dev-i386
       before_install:
-        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+        - mkdir bin
+        - ln -s /usr/bin/gcc-5 bin/gcc
+        - ln -s /usr/bin/g++-5 bin/g++
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env:
         - COMPILER="ccache /usr/bin/g++-5"
@@ -157,12 +161,15 @@ jobs:
           packages:
             - libwww-perl
             - clang-3.7
+            - g++-5
             - libstdc++-5-dev
             - libubsan0
             - parallel
             - libc6-dev-i386
       before_install:
-        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+        - mkdir bin
+        - ln -s /usr/bin/gcc-5 bin/gcc
+        - ln -s /usr/bin/c++-5 bin/g++
         - export CCACHE_CPP2=yes
       # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env:
@@ -184,11 +191,14 @@ jobs:
           packages:
             - libwww-perl
             - clang-3.7
+            - g++-5
             - libstdc++-5-dev
             - libubsan0
             - libc6-dev-i386
       before_install:
-        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+        - mkdir bin
+        - ln -s /usr/bin/gcc-5 bin/gcc
+        - ln -s /usr/bin/g++-5 bin/g++
         - export CCACHE_CPP2=yes
       # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env:
@@ -212,14 +222,75 @@ jobs:
             - g++-5
             - libc6-dev-i386
       before_install:
-        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+        - mkdir bin
+        - ln -s /usr/bin/gcc-5 bin/gcc
+        - ln -s /usr/bin/g++-5 bin/g++
       install:
         - ccache -z
         - ccache --max-size=1G
         - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE -j2)
 
+    # cmake build using g++-7
+    - stage: Test different OS/CXX/Flags
+      os: linux
+      compiler: gcc
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - g++-7
+            - libc6-dev-i386
+      before_install:
+        - mkdir bin
+        - ln -s /usr/bin/gcc-7 bin/gcc
+        - ln -s /usr/bin/g++-7 bin/g++
+      install:
+        - ccache -z
+        - ccache --max-size=1G
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release'  '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE -j2)
+
+    # cmake build using clang++-6
+    - stage: Test different OS/CXX/Flags
+      os: linux
+      compiler: clang
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+            - llvm-toolchain-trusty-6.0
+          packages:
+            - libwww-perl
+            - g++-5
+            - clang-6.0
+            - libstdc++-5-dev
+            - libubsan0
+            - parallel
+            - libc6-dev-i386
+      before_install:
+        - mkdir bin
+        # Use gcc/g++ 5 for tests, as Clang doesn't work yet
+        # See https://github.com/diffblue/cbmc/issues/2370 for details.
+        - ln -s /usr/bin/gcc-5 bin/gcc-5
+        - ln -s /usr/bin/g++-5 bin/g++-5
+      install:
+        - ccache -z
+        - ccache --max-size=1G
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-6.0' '-DCMAKE_CXX_FLAGS=-Qunused-arguments'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE -j2)
+
+    # cmake build on OSX, using default clang
     - stage: Test different OS/CXX/Flags
       os: osx
       compiler: clang

regression/cpp/auto2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.cpp
-
+-std=c++98
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cpp/auto3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.cpp
-
+-std=c++98
 ^EXIT=(64|1)$
 ^SIGNAL=0$
 parse error

src/goto-cc/gcc_mode.cpp

@@ -597,6 +597,11 @@ int gcc_modet::doit()
     if(std_string=="gnu++14" || std_string=="c++14")
       config.cpp.set_cpp14();
   }
+  else
+  {
+    config.ansi_c.c_standard = gcc_version.default_c_standard;
+    config.cpp.cpp_standard = gcc_version.default_cxx_standard;
+  }
 
   // gcc's default is 32 bits for wchar_t
   if(cmdline.isset("short-wchar"))

src/goto-cc/gcc_version.cpp

@@ -31,7 +31,8 @@ void gcc_versiont::get(const std::string &executable)
            "bcc 0 0 0\n"
            "#else\n"
            "gcc __GNUC__ __GNUC_MINOR__ __GNUC_PATCHLEVEL__\n"
-           "#endif\n";
+           "#endif\n"
+           "default_c_standard __STDC_VERSION__\n";
   }
 
   // some variants output stuff on stderr, say Apple LLVM,
@@ -52,23 +53,78 @@ void gcc_versiont::get(const std::string &executable)
     std::string line;
 
     while(!in.fail() && std::getline(in, line))
-      if(!line.empty() && line[0] != '#')
-        break;
-
-    auto split = split_string(line, ' ');
+    {
+      if(line.empty() || line[0] == '#')
+        continue;
+
+      auto split = split_string(line, ' ');
+
+      if(split.size() >= 4)
+      {
+        if(split[0] == "gcc")
+          flavor = flavort::GCC;
+        else if(split[0] == "bcc")
+          flavor = flavort::BCC;
+        else if(split[0] == "clang")
+          flavor = flavort::CLANG;
+
+        v_major = unsafe_string2unsigned(split[1]);
+        v_minor = unsafe_string2unsigned(split[2]);
+        v_patchlevel = unsafe_string2unsigned(split[3]);
+      }
+      else if(split.size() == 2 && split[0] == "default_c_standard")
+      {
+        if(split[1] == "199901L")
+          default_c_standard = configt::ansi_ct::c_standardt::C99;
+        else if(split[1] == "201112L")
+          default_c_standard = configt::ansi_ct::c_standardt::C11;
+      }
+    }
 
-    if(split.size() >= 4)
+    if(flavor == flavort::GCC || flavor == flavort::CLANG)
     {
-      if(split[0] == "gcc")
-        flavor = flavort::GCC;
-      else if(split[0] == "bcc")
-        flavor = flavort::BCC;
-      else if(split[0] == "clang")
-        flavor = flavort::CLANG;
-
-      v_major = unsafe_string2unsigned(split[1]);
-      v_minor = unsafe_string2unsigned(split[2]);
-      v_patchlevel = unsafe_string2unsigned(split[3]);
+      // Grab the default C++ standard. Unfortunately this requires another
+      // run, as the compiler can't preprocess two files in one go.
+
+      temporary_filet cpp_in("goto-gcc.", ".cpp");
+      temporary_filet cpp_out("goto-gcc.", ".out");
+      temporary_filet cpp_err("goto-gcc.", ".err");
+
+      {
+        std::ofstream out(cpp_in());
+        out << "default_cxx_standard __cplusplus\n";
+      }
+
+      int result = run(
+        executable,
+        {executable, "-E", "-x", "c++", "-", "-o", "-"},
+        cpp_in(),
+        cpp_out(),
+        cpp_err());
+
+      if(result >= 0)
+      {
+        std::ifstream in(cpp_out());
+        std::string line;
+
+        while(!in.fail() && std::getline(in, line))
+        {
+          if(line.empty() || line[0] == '#')
+            continue;
+
+          auto split = split_string(line, ' ');
+
+          if(split.size() == 2 && split[0] == "default_cxx_standard")
+          {
+            if(split[1] == "199711L")
+              default_cxx_standard = configt::cppt::cpp_standardt::CPP98;
+            else if(split[1] == "201103L")
+              default_cxx_standard = configt::cppt::cpp_standardt::CPP11;
+            else if(split[1] == "201402L")
+              default_cxx_standard = configt::cppt::cpp_standardt::CPP14;
+          }
+        }
+      }
     }
   }
 }

src/goto-cc/gcc_version.h

@@ -14,6 +14,8 @@ Date: May 2018
 #include <iosfwd>
 #include <string>
 
+#include <util/config.h>
+
 class gcc_versiont
 {
 public:
@@ -34,8 +36,17 @@ class gcc_versiont
     BCC
   } flavor;
 
+  configt::ansi_ct::c_standardt default_c_standard;
+  configt::cppt::cpp_standardt default_cxx_standard;
+
   gcc_versiont()
-    : v_major(0), v_minor(0), v_patchlevel(0), flavor(flavort::UNKNOWN)
+    :
+    v_major(0),
+    v_minor(0),
+    v_patchlevel(0),
+    flavor(flavort::UNKNOWN),
+    default_c_standard(configt::ansi_ct::c_standardt::C89),
+    default_cxx_standard(configt::cppt::cpp_standardt::CPP98)
   {
   }
 };

src/util/irep_ids.def

@@ -41,7 +41,7 @@ IREP_ID_ONE(member_name)
 IREP_ID_TWO(C_member_name, #member_name)
 IREP_ID_TWO(equal, =)
 IREP_ID_TWO(implies, =>)
-IREP_ID_TWO(iff, <=>)
+IREP_ID_TWO(iff, "<=>")
 IREP_ID_ONE(and)
 IREP_ID_ONE(nand)
 IREP_ID_ONE(or)