diff --git a/regression/goto-cl/version/main.c b/regression/goto-cl/version/main.c new file mode 100644 index 00000000000..f8b643afbf2 --- /dev/null +++ b/regression/goto-cl/version/main.c @@ -0,0 +1,4 @@ +int main() +{ + return 0; +} diff --git a/regression/goto-cl/version/version.desc b/regression/goto-cl/version/version.desc new file mode 100644 index 00000000000..4f8f53b8a1e --- /dev/null +++ b/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$ diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index cd655102651..7ac2a80baa2 100644 --- a/src/goto-cc/Makefile +++ b/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 diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp index 9e3ce6e63d6..8fc9f2c47c9 100644 --- a/src/goto-cc/ms_cl_mode.cpp +++ b/src/goto-cc/ms_cl_mode.cpp @@ -28,6 +28,7 @@ Author: CM Wintersteiger, 2006 #include #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"; diff --git a/src/goto-cc/ms_cl_version.cpp b/src/goto-cc/ms_cl_version.cpp new file mode 100644 index 00000000000..f695cfb796f --- /dev/null +++ b/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 +#include +#include +#include + +#include + +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; +} diff --git a/src/goto-cc/ms_cl_version.h b/src/goto-cc/ms_cl_version.h new file mode 100644 index 00000000000..90a3544d011 --- /dev/null +++ b/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 +#include + +#include + +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