From a43e4fad9612e7e99ff1b486a5c8776a3b71e670 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 4 Aug 2018 13:35:31 +0100 Subject: [PATCH 1/3] add is_directory to file_util.h --- src/util/file_util.cpp | 25 +++++++++++++++++++++++++ src/util/file_util.h | 3 +++ unit/Makefile | 1 + unit/util/file_util.cpp | 34 ++++++++++++++++++++++++++++++++++ 4 files changed, 63 insertions(+) create mode 100644 unit/util/file_util.cpp 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("")); +} From 5bc74567879b138099f413d2c80ac5d02dea570e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 24 Jul 2018 22:27:47 +0100 Subject: [PATCH 2/3] goto-cl: /Fo can set an output directory --- buildspec-windows.yml | 1 + regression/goto-cl/Fo/Fo-directory.desc | 8 ++++ regression/goto-cl/Fo/dir/dummy | 1 + regression/goto-cl/Fo/main1.c | 1 + regression/goto-cl/Fo/main2.c | 1 + regression/goto-cl/Makefile | 21 +++++++++++ src/goto-cc/compile.cpp | 12 +++++- src/goto-cc/compile.h | 5 ++- src/goto-cc/ms_cl_mode.cpp | 49 ++++++++++++++++--------- 9 files changed, 78 insertions(+), 21 deletions(-) create mode 100644 regression/goto-cl/Fo/Fo-directory.desc create mode 100644 regression/goto-cl/Fo/dir/dummy create mode 100644 regression/goto-cl/Fo/main1.c create mode 100644 regression/goto-cl/Fo/main2.c create mode 100644 regression/goto-cl/Makefile 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..30406d32454 --- /dev/null +++ b/regression/goto-cl/Fo/Fo-directory.desc @@ -0,0 +1,8 @@ +CORE + +/c main1.c main2.c /Fodir/ +^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 { From 4df2187f3517c442fefb601c9add8980d163ac85 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 3 Aug 2018 16:54:11 +0000 Subject: [PATCH 3/3] debugging output to resolve seg fault --- regression/goto-cl/Fo/Fo-directory.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/goto-cl/Fo/Fo-directory.desc b/regression/goto-cl/Fo/Fo-directory.desc index 30406d32454..df3e9feef62 100644 --- a/regression/goto-cl/Fo/Fo-directory.desc +++ b/regression/goto-cl/Fo/Fo-directory.desc @@ -1,6 +1,6 @@ CORE -/c main1.c main2.c /Fodir/ +--verbosity 10 /c main1.c main2.c /Fo dir ^EXIT=0$ ^SIGNAL=0$ --