Clean up run.h interface

src/goto-cc/as_mode.cpp

@@ -267,7 +267,7 @@ int as_modet::run_as()
   std::cout << '\n';
   #endif
 
-  return run(new_argv[0], new_argv, cmdline.stdin_file);
+  return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
 }
 
 int as_modet::as_hybrid_binary()

src/goto-cc/gcc_mode.cpp

@@ -835,7 +835,7 @@ int gcc_modet::preprocess(
     debug() << " " << new_argv[i];
   debug() << eom;
 
-  return run(new_argv[0], new_argv, cmdline.stdin_file, stdout_file);
+  return run(new_argv[0], new_argv, cmdline.stdin_file, stdout_file, "");
 }
 
 int gcc_modet::run_gcc(const compilet &compiler)
@@ -878,7 +878,7 @@ int gcc_modet::run_gcc(const compilet &compiler)
     debug() << " " << new_argv[i];
   debug() << eom;
 
-  return run(new_argv[0], new_argv, cmdline.stdin_file);
+  return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
 }
 
 int gcc_modet::gcc_hybrid_binary(compilet &compiler)

src/goto-cc/hybrid_binary.cpp

@@ -52,7 +52,7 @@ int hybrid_binary(
       "--remove-section", "goto-cc",
       "--add-section", "goto-cc=" + goto_binary_file, output_file};
 
-    result = run(objcopy_argv[0], objcopy_argv, "", "");
+    result = run(objcopy_argv[0], objcopy_argv);
   }
 
   // delete the goto binary
@@ -79,7 +79,7 @@ int hybrid_binary(
       "lipo", output_file, "-create", "-arch", "hppa7100LC", goto_binary_file,
       "-output", output_file };
 
-    result = run(lipo_argv[0], lipo_argv, "", "");
+    result = run(lipo_argv[0], lipo_argv);
   }
 
   // delete the goto binary

src/goto-cc/ld_mode.cpp

@@ -163,7 +163,7 @@ int ld_modet::run_ld()
     debug() << " " << new_argv[i];
   debug() << eom;
 
-  return run(new_argv[0], new_argv, cmdline.stdin_file, "");
+  return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
 }
 
 int ld_modet::ld_hybrid_binary(compilet &compiler)

src/goto-cc/linker_script_merge.cpp

@@ -696,7 +696,7 @@ int linker_script_merget::get_linker_script_data(
     debug() << " " << argv[i];
   debug() << eom;
 
-  int rc=run(argv[0], argv, linker_def_infile(), def_out_file);
+  int rc = run(argv[0], argv, linker_def_infile(), def_out_file, "");
   if(rc!=0)
     warning() << "Problem parsing linker script" << eom;
 

src/util/run.cpp

@@ -32,13 +32,9 @@ Date: August 2012
 #include <util/unicode.h>
 #include <util/signal_catcher.h>
 
-int run_shell(const std::string &command)
+int run(const std::string &what, const std::vector<std::string> &argv)
 {
-  std::string shell="/bin/sh";
-  std::vector<std::string> argv;
-  argv.push_back(shell);
-  argv.push_back(command);
-  return run(shell, argv, "", "", "");
+  return run(what, argv, "", "", "");
 }
 
 #ifndef _WIN32

src/util/run.h

@@ -15,13 +15,13 @@ Date: August 2012
 #include <string>
 #include <vector>
 
+int run(const std::string &what, const std::vector<std::string> &argv);
+
 int run(
   const std::string &what,
   const std::vector<std::string> &argv,
-  const std::string &std_input = "",
-  const std::string &std_output = "",
-  const std::string &std_error = "");
-
-int run_shell(const std::string &command);
+  const std::string &std_input,
+  const std::string &std_output,
+  const std::string &std_error);
 
 #endif // CPROVER_UTIL_RUN_H