Use CL version to determine target

regression/goto-cl/version/main.c

@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}

regression/goto-cl/version/version.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+^Visual Studio mode \d+\.\d+ (x86|x64|ARM)$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/goto-cc/Makefile

@@ -19,6 +19,7 @@ SRC = armcc_cmdline.cpp \
       linker_script_merge.cpp \
       ms_cl_cmdline.cpp \
       ms_cl_mode.cpp \
+      ms_cl_version.cpp \
       ms_link_cmdline.cpp \
       ms_link_mode.cpp \
       # Empty last line

src/goto-cc/ms_cl_mode.cpp

@@ -28,6 +28,7 @@ Author: CM Wintersteiger, 2006
 #include <util/prefix.h>
 
 #include "compile.h"
+#include "ms_cl_version.h"
 
 static bool has_directory_suffix(const std::string &path)
 {
@@ -59,11 +60,21 @@ int ms_cl_modet::doit()
   const auto verbosity = eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_ERROR, message_handler);
 
-  debug() << "Visual Studio mode" << eom;
+  ms_cl_versiont ms_cl_version;
+  ms_cl_version.get("cl.exe");
+
+  debug() << "Visual Studio mode " << ms_cl_version << eom;
 
   // get configuration
   config.set(cmdline);
 
+  if(ms_cl_version.target == ms_cl_versiont::targett::x86)
+    config.ansi_c.set_32();
+  else if(ms_cl_version.target == ms_cl_versiont::targett::ARM)
+    config.ansi_c.set_32();
+  else if(ms_cl_version.target == ms_cl_versiont::targett::x86)
+    config.ansi_c.set_64();
+
   config.ansi_c.mode=configt::ansi_ct::flavourt::VISUAL_STUDIO;
   compiler.object_file_extension="obj";
 

src/goto-cc/ms_cl_version.cpp

@@ -0,0 +1,90 @@
+/*******************************************************************\
+
+Module: Visual Studio CL version numbering scheme
+
+Author: Daniel Kroening, 2018
+
+\*******************************************************************/
+
+#include "ms_cl_version.h"
+
+#include <util/run.h>
+#include <util/string2int.h>
+#include <util/string_utils.h>
+#include <util/tempfile.h>
+
+#include <fstream>
+
+void ms_cl_versiont::get(const std::string &executable)
+{
+  // stdout will have the help output, we just want to discard it
+  temporary_filet tmp_file_out("goto-cl.", ".out");
+  // stderr has the version string
+  temporary_filet tmp_file_err("goto-cl.", ".err");
+  const int result =
+    run(executable, {executable}, "", tmp_file_out(), tmp_file_err());
+
+  v_major = v_minor = 0;
+  target = targett::UNKNOWN;
+
+  if(result >= 0)
+  {
+    std::ifstream in(tmp_file_err());
+    std::string line;
+
+    if(std::getline(in, line))
+    {
+      // Example:
+      //
+      // NOLINTNEXTLINE (whitespace/braces)
+      // Microsoft (R) 32-bit C/C++ Optimizing Compiler Version 15.00.30729.01 for 80x86
+      auto split = split_string(line, ' ');
+      if(split.size() > 3)
+      {
+        if(split.back() == "x86" || split.back() == "80x86")
+          target = targett::x86;
+        else if(split.back() == "x64")
+          target = targett::x64;
+        else if(split.back() == "ARM")
+          target = targett::ARM;
+        else
+          target = targett::UNKNOWN;
+
+        auto split_v = split_string(split[split.size() - 3], '.');
+
+        if(split_v.size() >= 2)
+        {
+          v_major = safe_string2unsigned(split_v[0]);
+          v_minor = safe_string2unsigned(split_v[1]);
+        }
+      }
+    }
+  }
+}
+
+bool ms_cl_versiont::is_at_least(unsigned _major, unsigned _minor) const
+{
+  return v_major > _major || (v_major == _major && v_minor >= _minor);
+}
+
+std::ostream &operator<<(std::ostream &out, const ms_cl_versiont &v)
+{
+  out << v.v_major << '.' << v.v_minor;
+
+  switch(v.target)
+  {
+  case ms_cl_versiont::targett::x86:
+    out << " x86";
+    break;
+  case ms_cl_versiont::targett::x64:
+    out << " x64";
+    break;
+  case ms_cl_versiont::targett::ARM:
+    out << " ARM";
+    break;
+  case ms_cl_versiont::targett::UNKNOWN:
+    break;
+  }
+
+  return out;
+}

src/goto-cc/ms_cl_version.h

@@ -0,0 +1,50 @@
+/*******************************************************************\
+
+Module: Visual Studio CL version numbering scheme
+
+Author: Daniel Kroening
+
+Date: August 2018
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_CC_MS_CL_VERSION_H
+#define CPROVER_GOTO_CC_MS_CL_VERSION_H
+
+#include <iosfwd>
+#include <string>
+
+#include <util/config.h>
+
+class ms_cl_versiont
+{
+public:
+  unsigned v_major, v_minor;
+
+  void get(const std::string &executable);
+
+  bool is_at_least(unsigned v_major, unsigned v_minor = 0) const;
+
+  configt::ansi_ct::c_standardt default_c_standard;
+  configt::cppt::cpp_standardt default_cxx_standard;
+
+  ms_cl_versiont()
+    : v_major(0),
+      v_minor(0),
+      default_c_standard(configt::ansi_ct::c_standardt::C89),
+      default_cxx_standard(configt::cppt::cpp_standardt::CPP98)
+  {
+  }
+
+  enum class targett
+  {
+    UNKNOWN,
+    x86,
+    x64,
+    ARM
+  } target;
+};
+
+std::ostream &operator<<(std::ostream &, const ms_cl_versiont &);
+
+#endif // CPROVER_GOTO_CC_MS_CL_VERSION_H