100# define BUFSIZE (1024 * 64)
127 :
log{message_handler}
141 std::string base_name =
"\\\\.\\pipe\\cbmc\\child\\";
144 const std::string
in_name = base_name +
"\\IN";
179 "Input pipe creation failed on SetHandleInformation");
181 const std::string
out_name = base_name +
"\\OUT";
210 "Output pipe creation failed on SetHandleInformation");
214 proc_info = std::make_unique<PROCESS_INFORMATION>();
280 char **args =
reinterpret_cast<char **
>(
304 <<
" failed with error: " << std::strerror(
errno) << std::endl;
369 log.
debug() <<
"Last error code is " + std::to_string(error_code)
377 log.
debug() <<
"Zero bytes send to sub process. Retrying in "
384 "Number of bytes written to sub process must match message size."
387 " bytes were written.");
405 "Can only receive() from a fully initialised process");
406 std::string
response = std::string(
"");
428 "More bytes cannot be read at a time, than the size of the buffer");
476# define WIN_POLL_WAIT 10
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
bool can_receive()
See if this process can receive data from the other process.
void wait_receivable(int wait_time)
Wait for the pipe to be ready, waiting specified time between checks.
std::string receive()
Read a string from the child process' output.
send_responset send(const std::string &message)
Send a string message (command) to the child process.
statet
Enumeration to keep track of child process state.
piped_processt(const std::vector< std::string > &commandvec, message_handlert &message_handler)
Initiate a new subprocess with pipes supporting communication between the parent (this process) and t...
statet get_status()
Get child process status.
send_responset
Enumeration for send response.
std::string wait_receive()
Wait until a string is available and read a string from the child process' output.
Thrown when some external system fails unexpectedly.
int fcntl(int fd, int cmd,...)
int __CPROVER_ID java::java io InputStream read
Subprocess communication with pipes.
#define PIPED_PROCESS_INFINITE_TIMEOUT
int kill(pid_t pid, int sig)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
FILE * fdopen(int handle, const char *mode)
int fputs(const char *s, FILE *stream)
void * malloc(__CPROVER_size_t malloc_size)
char * strdup(const char *str)
std::wstring widen(const char *s)
int usleep(unsigned int usec)