7 /*@observer@*/ const void *data
;
11 struct pipe_outbuffer
{
12 /*@only@*/ /*@null@*/ void *data
;
16 extern int pipethrough(const char *command
,
17 const struct pipe_inbuffer
*stdin_buf
,
18 /*@out@*/ struct pipe_outbuffer
*stdout_buf
,
19 /*@out@*/ struct pipe_outbuffer
*stderr_buf
,
20 /*@out@*/ int *status
)
21 /*@globals internalState, fileSystem, errno, stderr; @*/
22 /*@modifies internalState, fileSystem, errno, *stderr, *stdout_buf, *stderr_buf, *status; @*/;
24 extern void pipe_outbuffer_finalize(/*@special@*/ struct pipe_outbuffer
*buf
)
26 /*@releases buf->data; @*/
27 /*@ensures isnull buf->data; @*/;