kaih@khms.westfalen.de (Kai Henningsen) said:
> vonbrand@sleipnir.valparaiso.cl (Horst von Brand) wrote on 02.01.00 in <200001021555.MAA01783@sleipnir.valparaiso.cl>:
[...]
> > 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.
> I'm not quite sure if you think it's going to find too many or too few
> bugs.
Way too many false positives for real usefullness. A long time ago, when
the kernel sources were much smaller, somebody ran lclint on them and got
something like 500Kb of output (I seem to remember after compression). For
code that might at that point have had a dozen or so programming errors it
would catch, not exactly cost-effective.
> Anyway, as anyone who's done mathematical proofs knows, you don't really
> need the fully general thing anyway. That's what you have a programmer
> for. You tell the thing what is supposed to happen, and the thing verifies
> that this is indeed what happens, or otherwise tells you that it can't
> figure this out and you'll have to look for yourself.
Yes. Now: How do you explain this "Has to happen" to the programmer and the
program in terms they both understand? If Linus says "This function must
not be called in interrupt context", or "Make sure there is no race when
updating the foo list", I'd understand; the program won't. To describe that
in some precise language might be much longer than the code so annotated.
Who then says there are no more bugs in the annotation than in the original
code? What if I go in and change the code, but don't update the
description (because I don't understand it, or out of plain lazyness)?
[...]
> > 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.
>
> Also because, while there was a free gcc, there wasn't a free lint for
> quite a long time.
Because ANSI C + gcc -Wall do most of the job anyway.
-- Dr. Horst H. von Brand mailto:vonbrand@inf.utfsm.cl Departamento de Informatica Fono: +56 32 654431 Universidad Tecnica Federico Santa Maria +56 32 654239 Casilla 110-V, Valparaiso, Chile Fax: +56 32 797513- 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 : Fri Jan 07 2000 - 21:00:09 EST