diff options
author | dzwdz | 2021-09-18 09:37:53 +0200 |
---|---|---|
committer | dzwdz | 2021-09-18 09:37:53 +0200 |
commit | 8e757fae5aaece57755a98544f193bc2672966b3 (patch) | |
tree | 37ac93907323941a3bb3de2edb2fc08ca821360e /src/shared/types.h | |
parent | 7a44fc5381dabb65dfdb667dc442108d0465799a (diff) |
merge `kernel/types.h` and `init/types.h`
Diffstat (limited to 'src/shared/types.h')
-rw-r--r-- | src/shared/types.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/shared/types.h b/src/shared/types.h new file mode 100644 index 0000000..5dd39ad --- /dev/null +++ b/src/shared/types.h @@ -0,0 +1,10 @@ +#pragma once +#include <stdint.h> + +#ifdef __CHECKER__ +# define __user __attribute__((noderef, address_space(__user))) +#else +# define __user +#endif + +typedef void __user * userptr_t; |