on Windows, empty shell arguments require quotes

Unix-like OSs pass an array of strings to processes as the command line
arguments. Empty arguments do not require special treatment.

By contrast, Windows uses a single string to pass all arguments to the
process.  The process parses the string to construct argv[].  To pass an
empty argument, quotes are required.

Note that this is unrelated to any additional parsing a shell might perform.

Author: Daniel Kroening

src/util/run.cpp

@@ -165,7 +165,8 @@ static fdt stdio_redirection(int fd, const std::string &file)
 // https://blogs.msdn.microsoft.com/twistylittlepassagesallalike/2011/04/23/everyone-quotes-command-line-arguments-the-wrong-way/
 std::wstring quote_windows_arg(const std::wstring &src)
 {
-  if(src.find_first_of(L" \t\n\v\"") == src.npos)
+  // note that an empty argument requires quotes
+  if(src.find_first_of(L" \t\n\v\"") == src.npos && !src.empty())
     return src;
 
   std::wstring result = L"\"";