2 /** \file pipethrough.h
3 * \brief Header: a module for piping
5 * Pipe a buffer through a child command and receive two containing
6 * the stdout and stderr output of the child process.
14 struct pipe_inbuffer
{
15 /*@observer@*/ const void *data
;
19 struct pipe_outbuffer
{
20 /*@only@*/ /*@null@*/ void *data
;
24 extern int pipethrough(const char *command
,
25 const struct pipe_inbuffer
*stdin_buf
,
26 /*@out@*/ struct pipe_outbuffer
*stdout_buf
,
27 /*@out@*/ struct pipe_outbuffer
*stderr_buf
,
28 /*@out@*/ int *status
)
29 /*@globals internalState, fileSystem, errno, stderr; @*/
30 /*@modifies internalState, fileSystem, errno, *stderr, *stdout_buf, *stderr_buf, *status; @*/;
32 extern void pipe_outbuffer_finalize(/*@special@*/ struct pipe_outbuffer
*buf
)
34 /*@releases buf->data; @*/
35 /*@ensures isnull buf->data; @*/;