[ Resend - accidentally sent it as a private reply instead of to the list...]
> Is this 'super-lint' something that could/should be implemented in
> something like 'cxref' and included in documentation?
This super-lint is not something that you're going to toss into cxref. It's a
hard problem.
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.
I believe that what I have now is on the right track to a workable tool (which
is saying a lot considering the number of dead-ends I've gone down), but it
still needs quite a lot of work.
Jeff
-
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/
This archive was generated by hypermail 2b29 : Sat Jan 01 2000 - 23:11:58 EST