goto-cl: /Fo can set an output directory

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"

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$

regression/goto-cl/Fo/dir/dummy

@@ -0,0 +1 @@
+// blank

regression/goto-cl/Fo/main1.c

@@ -0,0 +1 @@
+// blank

regression/goto-cl/Fo/main2.c

@@ -0,0 +1 @@
+// blank

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

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;

src/goto-cc/compile.h

@@ -45,7 +45,10 @@ class compilet:public language_uit
   std::list<irep_idt> 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);
 

src/goto-cc/ms_cl_mode.cpp

@@ -21,23 +21,24 @@ Author: CM Wintersteiger, 2006
 
 #include <iostream>
 
-#include <util/message.h>
-#include <util/prefix.h>
 #include <util/config.h>
+#include <util/file_util.h>
 #include <util/get_base_name.h>
+#include <util/message.h>
+#include <util/prefix.h>
 
 #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,24 +104,36 @@ 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"))
   {
     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
   {

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
+}

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

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 \

unit/util/file_util.cpp

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: Unit tests for file_util.h
+
+Author: Daniel Kroening
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <util/file_util.h>
+#include <util/tempdir.h>
+#include <util/unicode.h>
+
+#include <fstream>
+
+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(""));
+}