diff options
| author | Linus Torvalds <torvalds@penguin.transmeta.com> | 2003-04-08 03:10:42 -0700 |
|---|---|---|
| committer | Linus Torvalds <torvalds@home.transmeta.com> | 2003-04-08 03:10:42 -0700 |
| commit | 475cd853695f577664e20e4a907bf8b0a5740af0 (patch) | |
| tree | c14d28f3760bffb46cb04870836fdbb0231f2dc4 /include/linux | |
| parent | deeefec860847a1cc72e822c2b5c4ae542894490 (diff) | |
Add __user/__kernel address space modifiers. When not
checking, these end up being no-ops, but they get enabled
by the type checker as special address_space attributes.
Diffstat (limited to 'include/linux')
| -rw-r--r-- | include/linux/compiler.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/include/linux/compiler.h b/include/linux/compiler.h index a28d0d51b851..6cbab5a2c88b 100644 --- a/include/linux/compiler.h +++ b/include/linux/compiler.h @@ -1,6 +1,14 @@ #ifndef __LINUX_COMPILER_H #define __LINUX_COMPILER_H +#ifdef __CHECKER__ + #define __user __attribute__((address_space(1))) + #define __kernel /* default address space */ +#else + #define __user + #define __kernel +#endif + #if (__GNUC__ > 3) || (__GNUC__ == 3 && __GNUC_MINOR__ >= 1) #define inline __inline__ __attribute__((always_inline)) #define __inline__ __inline__ __attribute__((always_inline)) |