> This super-lint is not something that you're going to toss into cxref.
> It's a hard problem.
One start in that direction (that I don't particularly like, BTW, as it
needs much assistance from the programmer, and seems to make certain legal
constructions like handling linked lists totally impossible) is lclint,
from somewhere on MIT AFAIR.
> I spent quite a while working on exactly this. I got fed up with it about a
> year ago and decided to do something easier, like porting the kernel to
> user-space.
> What I have is essentially a theorem-prover, with the theorems to be
> proved generated from the code being analyzed. E.g. "x[i] = 0" would
> generate the following theorems: "x is a valid pointer, the low bound of
> x is <= 0, and the high bound of x is >= i". It would backtrack through
> the code along every path reaching the "x[i] = 0" proving in each case
> that the theorems are true or that the path is logically impossible.
For full generality you need a complete and sound formal semantic for
C. And that is _extremely_ hard, if indeed possible. In the end, you will
hit the halting problem, so you will _always_ underestimate the "can't
happen", and that is exactly what irritates me the most of such tools.
BTW, much of what you are describing is exactly what the compiler has to do
to discover optimization oportunities. I assume that is why lints fell
into disfavour, partly because of ANSI C prototypes (the original lint
served mostly to detect mismatches between declarations and uses) and stuff
like gcc's -Wall can be had almost for free in the compiler.
-- Horst von Brand vonbrand@sleipnir.valparaiso.cl Casilla 9G, Viņa del Mar, Chile +56 32 672616- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.tux.org/lkml/