Re: [Tinycc-devel] Attributes for __user

[Dave Long]

> It seems that gcc does not support it yet (am it right ?), but adding 
> support for 'noderef' and 'address_space(N)' attributes would be easy in 
> TinyCC. It would allow to do interesting checks of the Linux kernel.

As well as other code.  Ten years ago,
the trouble with vectorizing C code was
that one never could be sure what had
been changed after a pointer write.

C99's "restrict" probably addresses this
issue, but code proofs (and optimizations
which rely on such knowledge) might be a
bit easier if pointers which were pointing
into different data structures were known
as such to the toolchain.

-Dave

:: :: ::

CAR Hoare, on pointers being data's GOTO:
> References are like jumps, leading wildly from one part of a data
> structure to another.