diff --git a/kernel/cobalt/pipe.c b/kernel/cobalt/pipe.c
index 0b8f8cbf8317f9cbe8a3036d4439e319dd306c3c..16e85125c41412ab0b92482087833c6c8e4e8830 100644
--- a/kernel/cobalt/pipe.c
+++ b/kernel/cobalt/pipe.c
@@ -28,6 +28,7 @@
 #include <linux/device.h>
 #include <linux/uaccess.h>
 #include <asm/io.h>
+#include <asm/xenomai/syscall.h>
 #include <cobalt/kernel/sched.h>
 #include <cobalt/kernel/heap.h>
 #include <cobalt/kernel/pipe.h>
@@ -795,7 +796,7 @@ static ssize_t xnpipe_read(struct file *file,
 	ssize_t ret;
 	spl_t s;
 
-	if (!access_ok(VERIFY_WRITE, buf, count))
+	if (!access_wok(buf, count))
 		return -EFAULT;
 
 	xnlock_get_irqsave(&nklock, s);
@@ -903,7 +904,7 @@ static ssize_t xnpipe_write(struct file *file,
 	if (count == 0)
 		return 0;
 
-	if (!access_ok(VERIFY_READ, buf, count))
+	if (!access_rok(buf, count))
 		return -EFAULT;
 
 	xnlock_get_irqsave(&nklock, s);