#ifndef SYSCALL_IPCPIPE_H_
#define SYSCALL_IPCPIPE_H_

#include <stdint.h>
#include <stddef.h>
#include "syscall/syscall.h"

int32_t SYSCALL4(sys_ipc_piperead, pid1, pipenum1, buffer1, len1);
int32_t SYSCALL4(sys_ipc_pipewrite, pid1, pipenum1, buffer1, len1);
int32_t SYSCALL1(sys_ipc_pipemake, pipenum1);
int32_t SYSCALL1(sys_ipc_pipedelete, pipenum1);
int32_t SYSCALL4(sys_ipc_pipeconnect, pid1, pipenum1, pid2, pipenum2);

#endif // SYSCALL_IPCPIPE_H_