1 files changed, 8 insertions, 1 deletions
diff --git a/src/kernel/types.h b/src/kernel/types.h
index 891e644..44a0d46 100644
--- a/src/kernel/types.h
+++ b/src/kernel/types.h
@@ -2,4 +2,11 @@
 #include <stdint.h>
 
 #define TYPES_INCLUDED
-typedef uintptr_t user_ptr;
+
+#ifdef __CHECKER__
+#  define __user __attribute__((noderef, address_space(__user)))
+#else
+#  define __user
+#endif
+
+typedef void __user * userptr_t;