diff --git a/buildspec-windows.yml b/buildspec-windows.yml index adc9209d100..a8abb6fbc0d 100644 --- a/buildspec-windows.yml +++ b/buildspec-windows.yml @@ -63,6 +63,7 @@ phases: - | $env:Path = "C:\tools\cygwin\bin;$env:Path" cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" ' + cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/goto-cl test BUILD_ENV=MSVC" ' - | $env:Path = "C:\tools\cygwin\bin;$env:Path" diff --git a/regression/goto-cl/Fo/Fo-directory.desc b/regression/goto-cl/Fo/Fo-directory.desc new file mode 100644 index 00000000000..df3e9feef62 --- /dev/null +++ b/regression/goto-cl/Fo/Fo-directory.desc @@ -0,0 +1,8 @@ +CORE + +--verbosity 10 /c main1.c main2.c /Fo dir +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/goto-cl/Fo/dir/dummy b/regression/goto-cl/Fo/dir/dummy new file mode 100644 index 00000000000..859ed91d505 --- /dev/null +++ b/regression/goto-cl/Fo/dir/dummy @@ -0,0 +1 @@ +// blank diff --git a/regression/goto-cl/Fo/main1.c b/regression/goto-cl/Fo/main1.c new file mode 100644 index 00000000000..859ed91d505 --- /dev/null +++ b/regression/goto-cl/Fo/main1.c @@ -0,0 +1 @@ +// blank diff --git a/regression/goto-cl/Fo/main2.c b/regression/goto-cl/Fo/main2.c new file mode 100644 index 00000000000..859ed91d505 --- /dev/null +++ b/regression/goto-cl/Fo/main2.c @@ -0,0 +1 @@ +// blank diff --git a/regression/goto-cl/Makefile b/regression/goto-cl/Makefile new file mode 100644 index 00000000000..9a84b463396 --- /dev/null +++ b/regression/goto-cl/Makefile @@ -0,0 +1,21 @@ +default: tests.log + +test: + @../test.pl -p -c ../../../src/goto-cc/goto-cl + +tests.log: ../test.pl + @../test.pl -p -c ../../../src/goto-cc/goto-cl + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + find -name '*.obj' -execdir $(RM) '{}' \; + find -name '*.goto-cc-saved' -execdir $(RM) '{}' \; + $(RM) tests.log diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index e83b1192da4..705e034eca5 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -421,9 +421,17 @@ bool compilet::compile() std::string cfn; if(output_file_object=="") - cfn=get_base_name(file_name, true)+"."+object_file_extension; + { + const std::string file_name_with_obj_ext = + get_base_name(file_name, true) + "." + object_file_extension; + + if(!output_directory_object.empty()) + cfn = concat_dir_file(output_directory_object, file_name_with_obj_ext); + else + cfn = file_name_with_obj_ext; + } else - cfn=output_file_object; + cfn = output_file_object; if(write_object_file(cfn, symbol_table, compiled_functions)) return true; diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index 920d01378ae..cc2295ea8ea 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -45,7 +45,10 @@ class compilet:public language_uit std::list seen_modes; std::string object_file_extension; - std::string output_file_object, output_file_executable; + std::string output_file_executable; + + // the two options below are mutually exclusive -- use either or + std::string output_file_object, output_directory_object; compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror); diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp index 08d845c1bab..14d1db20056 100644 --- a/src/goto-cc/ms_cl_mode.cpp +++ b/src/goto-cc/ms_cl_mode.cpp @@ -21,23 +21,24 @@ Author: CM Wintersteiger, 2006 #include -#include -#include #include +#include #include +#include +#include #include "compile.h" -/// does it. -static bool is_directory(const std::string &s) +static bool has_directory_suffix(const std::string &path) { - if(s.empty()) - return false; - char last_char=s[s.size()-1]; - // Visual CL recognizes both - return last_char=='\\' || last_char=='/'; + // MS CL decides whether a parameter is a directory on the + // basis of the / or \\ suffix; it doesn't matter + // whether the directory actually exists. + return path.empty() ? false : + path.back()=='/' || path.back()=='\\'; } +/// does it. int ms_cl_modet::doit() { if(cmdline.isset('?') || @@ -103,13 +104,18 @@ int ms_cl_modet::doit() if(cmdline.isset("Fo")) { - compiler.output_file_object=cmdline.get_value("Fo"); + std::string Fo_value = cmdline.get_value("Fo"); - // this could be a directory - if(is_directory(compiler.output_file_object) && - cmdline.args.size()>=1) - compiler.output_file_object+= - get_base_name(cmdline.args[0], true)+".obj"; + // this could be a directory or a file name + if(has_directory_suffix(Fo_value)) + { + compiler.output_directory_object = Fo_value; + + if(!is_directory(Fo_value)) + warning() << "not a directory: " << Fo_value << eom; + } + else + compiler.output_file_object = Fo_value; } if(cmdline.isset("Fe")) @@ -117,10 +123,17 @@ int ms_cl_modet::doit() compiler.output_file_executable=cmdline.get_value("Fe"); // this could be a directory - if(is_directory(compiler.output_file_executable) && - cmdline.args.size()>=1) + if( + has_directory_suffix(compiler.output_file_executable) && + cmdline.args.size() >= 1) + { + if(!is_directory(compiler.output_file_executable)) + warning() << "not a directory: " + << compiler.output_file_executable << eom; + compiler.output_file_executable+= - get_base_name(cmdline.args[0], true)+".exe"; + get_base_name(cmdline.args[0], true) + ".exe"; + } } else { diff --git a/src/util/file_util.cpp b/src/util/file_util.cpp index 8c3c17ba3a5..0e8cfc80ddf 100644 --- a/src/util/file_util.cpp +++ b/src/util/file_util.cpp @@ -145,3 +145,28 @@ std::string concat_dir_file( file_name : directory+"/"+file_name; #endif } + +bool is_directory(const std::string &path) +{ + if(path.empty()) + return false; + +#ifdef _WIN32 + + auto attributes = ::GetFileAttributesW(widen(path).c_str()); + if (attributes == INVALID_FILE_ATTRIBUTES) + return false; + else + return (attributes & FILE_ATTRIBUTE_DIRECTORY) != 0; + +#else + + struct stat buf; + + if(stat(path.c_str(), &buf)!=0) + return false; + else + return (buf.st_mode & S_IFDIR) != 0; + +#endif +} diff --git a/src/util/file_util.h b/src/util/file_util.h index 54ed17e16c3..9cf259a3aac 100644 --- a/src/util/file_util.h +++ b/src/util/file_util.h @@ -19,4 +19,7 @@ std::string get_current_working_directory(); std::string concat_dir_file(const std::string &directory, const std::string &file_name); +// C++17 will allow us to use std::filesystem::is_directory() +bool is_directory(const std::string &path); + #endif // CPROVER_UTIL_FILE_UTIL_H diff --git a/unit/Makefile b/unit/Makefile index 53a17feda52..8757d39c42b 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -28,6 +28,7 @@ SRC += unit_tests.cpp \ solvers/refinement/string_refinement/union_find_replace.cpp \ util/expr.cpp \ util/expr_cast/expr_cast.cpp \ + util/file_util.cpp \ util/get_base_name.cpp \ util/graph.cpp \ util/irep.cpp \ diff --git a/unit/util/file_util.cpp b/unit/util/file_util.cpp new file mode 100644 index 00000000000..8cf4c5bd6f1 --- /dev/null +++ b/unit/util/file_util.cpp @@ -0,0 +1,34 @@ +/*******************************************************************\ + +Module: Unit tests for file_util.h + +Author: Daniel Kroening + +\*******************************************************************/ + +#include + +#include +#include +#include + +#include + +TEST_CASE("is_directory functionality", "[core][util][file_util]") +{ + temp_dirt temp_dir("testXXXXXX"); + + #ifdef _WIN32 + std::ofstream outfile(widen(temp_dir("file"))); + #else + std::ofstream outfile(temp_dir("file")); + #endif + + outfile.close(); + + REQUIRE(is_directory(temp_dir.path)); + REQUIRE(is_directory(temp_dir.path+"/")); + REQUIRE(!is_directory(temp_dir("whatnot"))); + REQUIRE(!is_directory(temp_dir("file"))); + REQUIRE(!is_directory("")); +}