CBMC
run.cpp File Reference
#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"
+ Include dependency graph for run.cpp:

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 More...
 
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. More...
 
std::string shell_quote (const std::string &src)
 quote a string for bash and CMD More...
 
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. More...
 

Typedef Documentation

◆ fdt

using fdt = int

Definition at line 59 of file run.cpp.

Function Documentation

◆ run() [1/3]

int run ( const std::string &  what,
const std::vector< std::string > &  argv 
)

Definition at line 48 of file run.cpp.

◆ run() [2/3]

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.

Definition at line 252 of file run.cpp.

◆ run() [3/3]

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.

Definition at line 524 of file run.cpp.

◆ shell_quote()

std::string shell_quote ( const std::string &  src)

quote a string for bash and CMD

This performs shell quoting if necessary on input src.

Definition at line 451 of file run.cpp.

◆ stdio_redirection()

static fdt stdio_redirection ( int  fd,
const std::string &  file 
)
static

open given file to replace either stdin, stderr, stdout

Definition at line 63 of file run.cpp.