Re: [Tinycc-devel] Attributes for __user

[Peter \"Firefly\" Lund]

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?

> 2) A pointer to an 'address_space(N)' data is only type-compatible with
> a pointer to the same address_space. It causes a warning if it is not.
>
> At the same time, support for 'volatile' and 'const' typing could be added.
>
> Any comments ?

I think I like it :)

-Peter

We bomb for peace on Mondays, Wednesdays and Fridays.  We bring democracy by 
bypassing
the UN voting process on Tuesdays, Thursdays and Saturdays...- Rogerborg