On Sat, Mar 20, 2010 at 08:53:12PM +0200, Mateusz Kocielski wrote:
> 2010/3/20 Thor Lancelot Simon <tls%panix.com@localhost>:
> > What is the benefit of this when compared to existing static-analysis
> > tools such as Coverity Scan, splint, or the Clang static analyzer? ÂWill
> > this cover any cases they don't? ÂIf so, which ones?
>
> Undecidability is the limit for static-analysis. Consider following program:
>
> *bzzzz*
> $ cat splint.c
> #include <stdio.h>
> #include <stdlib.h>
> #include <string.h>
>
> int main(int argc, char **argv)
> {
> int i;
> char blah[10];
> memset(blah, 0, sizeof(blah));
> if ( argc > 1 )
> i = atoi(argv[1]);
> else
> i = 0;
> printf("%d - %c\n", i, blah[i]);
> return 0;
> }
> $ splint splint.c
> Splint 3.1.2 --- 07 Sep 2009
> Finished checking --- no warnings
> $ ./splint 99
> 99 - 1
> *bzzzz*
>
> Static analysis used in splint is not strong enough to uncover bug.
> For sure there exists static analysis which is able to find this bug,
> but it might be a good subject for PhD thesis. :)
For what it's worth, here is what devel/frama-c has to say about this
sample, with frama-c -val splint.c:
splint.c:14:[kernel] warning: accessing out of bounds index. assert ((0 â i) â
(i < 10));
splint.c:14:[kernel] warning: accessing uninitialized left-value blah[i]:
assert(TODO)
splint.c:14:[kernel] warning: completely unspecified value in {{
blah -> [0..72],0%8 ;}} (size:<8>). This path is assumed to
be dead.
However, the results are much more difficult to analyse with examples
from our source tree. However, with ASCL annotations, it could be very
interesting to use it to a larger scale.
regards,
antoine
Attachment:
pgpOlg2j9yrV6.pgp
Description: PGP signature