[cfe-dev] Static Analyzer Rocks Hard

[Holger Schurig]

On Wednesday 25 June 2008 18:49:06 Ted Kremenek wrote:
> Another kind of "taint property" is tracking the use of
> kernel/user pointers in kernel space; this is more of an
> address-space qualifier problem, but it can also be viewed as
> a form of taint propagation.

AFAIK this is done e.g. by the sparse tool when you compile linux
with "make C=1".

In include/linux/compiler.h there are all the things defined that
sparse supports:

#ifdef __CHECKER__
# define __user         __attribute__((noderef, address_space(1)))
# define __kernel       /* default address space */
# define __safe         __attribute__((safe))
# define __force        __attribute__((force))
# define __nocast       __attribute__((nocast))
# define __iomem        __attribute__((noderef, address_space(2)))
# define __acquires(x)  __attribute__((context(x,0,1)))
# define __releases(x)  __attribute__((context(x,1,0)))
# define __acquire(x)   __context__(x,1)
# define __release(x)   __context__(x,-1)
# define __cond_lock(x,c)       ((c) ? ({ __acquire(x); 1; }) : 0)
#else
# define __user
# define __kernel
# define __safe
# define __force
# define __nocast
# define __iomem
# define __acquires(x)
# define __releases(x)
# define __acquire(x) (void)0
# define __release(x) (void)0
# define __cond_lock(x,c) (c)
#endif