goto-cl: /Fo can set an output directory

Author: Daniel Kroening

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
+
+/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;
+      {
+        std::string file_name =
+          get_base_name(file_name, true) + "." + object_file_extension;
+
+        if(!output_directory_object.empty())
+          cfn = concat_dir_file(output_directory_object, file_name);
+        else
+          cfn = file_name;
+      }
       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,15 @@ 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)
-{
-  if(s.empty())
-    return false;
-  char last_char=s[s.size()-1];
-  // Visual CL recognizes both
-  return last_char=='\\' || last_char=='/';
-}
-
 int ms_cl_modet::doit()
 {
   if(cmdline.isset('?') ||
@@ -103,24 +95,26 @@ 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(is_directory(Fo_value))
+      compiler.output_directory_object = Fo_value;
+    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)
-      compiler.output_file_executable+=
-        get_base_name(cmdline.args[0], true)+".exe";
+    if(
+      is_directory(compiler.output_file_executable) &&
+      cmdline.args.size() >= 1)
+      compiler.output_file_executable = concat_dir_file(
+        compiler.output_file_executable,
+        get_base_name(cmdline.args[0], true) + ".exe");
   }
   else
   {