CBMC
|
#include "run.h"
#include <cstring>
#include <cerrno>
#include <cstdio>
#include <cstdlib>
#include <fcntl.h>
#include <signal.h>
#include <sys/stat.h>
#include <sys/wait.h>
#include <unistd.h>
#include <fstream>
#include "invariant.h"
#include "signal_catcher.h"
Go to the source code of this file.
Typedefs | |
using | fdt = int |
Functions | |
int | run (const std::string &what, const std::vector< std::string > &argv) |
static fdt | stdio_redirection (int fd, const std::string &file) |
open given file to replace either stdin, stderr, stdout | |
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) |
This runs the executable given by the file name what . | |
std::string | shell_quote (const std::string &src) |
quote a string for bash and CMD | |
int | run (const std::string &what, const std::vector< std::string > &argv, const std::string &std_input, std::ostream &std_output, const std::string &std_error) |
This runs the executable given by the file name what . | |
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 | ||
) |
This runs the executable given by the file name what
.
Control returns when execution has finished. Stdin, stdout and stderr may be redirected from/to a given file. Give the empty string to retain the default handle. Any shell-meta characters in the executable, argv
and the I/O redirect files are escaped as needed.
int run | ( | const std::string & | what, |
const std::vector< std::string > & | argv, | ||
const std::string & | std_input, | ||
std::ostream & | std_output, | ||
const std::string & | std_error | ||
) |
This runs the executable given by the file name what
.
Control returns when execution has finished. Stdin and stderr may be redirected from/to a given file. Give the empty string to retain the default handle. Any output to stdout is stored in the std_output
stream buffer. Any shell-meta characters in the executable, argv
and the I/O redirect files are escaped as needed.
std::string shell_quote | ( | const std::string & | src | ) |