On Thu, 24 Apr 2003, Fabrice Bellard wrote:
I have seen that the keyword __user was added recently in the Linux
kernel to indicate "user data" so that compile time checks can be done
with appropriate tools.
__user is defined as (in linux/compile.h):
#ifdef __CHECKER__
#define __user __attribute__((noderef, address_space(1)))
#define __kernel /* default address space */
#else
#define __user
#define __kernel
#endif
It seems that gcc does not support it yet (am it right ?), but adding
AFAIK, it is not supposed to. It is there for the benefit of the Stanford
Checker.
support for 'noderef' and 'address_space(N)' attributes would be easy in
TinyCC. It would allow to do interesting checks of the Linux kernel.
The semantics could be the following:
1) Dereferencing a pointer pointing to data with the 'noderef' attribute
causes a warning.
But such pointers could be cast to other types so dereferences can still
take place as long as the programmer demonstrates that s/h/it knows what
they are doing, right?