Simple IPC with pipes

user/init/main.c

@@ -1,8 +1,10 @@
 #include <stdint.h>
-#include <sysdefs/ioctl.h>
-#include <system/system.h>
-#include <system/ioctl.h>
 #include <string/string.h>
+#include <system/system.h>
+#include <sysdefs/ioctl.h>
+#include <system/ioctl.h>
+#include <sysdefs/ipcpipe.h>
+#include <system/ipcpipe.h>
 
 void main(void) {
   debugprint("Hello world from userspace in C");
@@ -18,5 +20,10 @@ void main(void) {
   debugprint(buf);
 
   ioctl_closefile(ioh);
+
+  char *aba = "Hello!";
+  ipcpipe(IPCPIPE_SELFPID, IPCPIPE_OUT, IPCPIPE_WRITE, (uint8_t *)aba, string_len(aba));
+
+  for(;;);
 }