Re: Is splint the best for static code checking? I mean free.

Bin Chen wrote:
But I have some doubts, such as following code checked by splint:

binch@binch:/tmp$ splint b.c
Splint 3.1.1 --- 20 Jun 2006

b.c: (in function main)
b.c:6:2: Path with no return in function declared to return int
There is a path through a function declared to return a value on
which there is no return statement. This means the execution may fall
through without returning a meaningful result to the caller. (Use
-noret to inhibit warning)

b.c:1:5: Variable exported but not used outside b: b
A declaration is exported, but not used outside this module.
Declaration can use static qualifier. (Use -exportlocal to inhibit
warning)

Finished checking --- 2 code warnings

binch@binch:/tmp$ cat b.c

int b[3];

main() { b[8] = 5; }

It can't figure out the array overflow access. Any other choice to
splint? I need a free one. Thanks. abai

First of all, static analysis is a method that might induce some false
positive alarms. Meaning that splint might detect "errors" that turn to
be proper behavior when looked at.

It comes from the simplifications made by splint to run faster (and to
terminate) which are over-approximations.

Second, the code you are presenting has no overflow as long as dead-code
is removed... and splint does say that as you have no way out for the
data, it will be removed.

But, in any case, don't rely too much on splint (and on any static
analysis tools). They only cover _partially_ the bugs that you might put
into your code and might raise false positives. They are quite useful to
automate and systematize the search of stupid and common bugs but of no
use for some more advanced ones.

Regards
--
Emmanuel Fleury | Room: 261
Associate Professor, | Phone: +33 (0)5 40 00 69 34
LaBRI, Domaine Universitaire | Fax: +33 (0)5 40 00 66 69
351, Cours de la Libération | Email: emmanuel.fleury@xxxxxxxx
33405 Talence Cedex, France | URL: http://www.labri.fr/~fleury
.

Relevant Pages

  • Re: Question about a splint diagnostic
    ... When I issue "splint u1.c u2.c" I get ... Finished checking --- 1 code warning ... typedef extern int Q; ... that this happens because one only links with the libraries ...
    (comp.lang.c)
  • Re: Question about a splint diagnostic
    ... When I issue "splint u1.c u2.c" I get ... Finished checking --- 1 code warning ... typedef extern int Q; ... that this happens because one only links with the libraries ...
    (comp.lang.c)
  • Re: lint warning
    ... So that I wrote simple c program as mentioned bellow ... to put up with in splint. ... PC-lint is worth the money if you are serious about ...
    (comp.lang.c)
  • Re: lint warning
    ... So that I wrote simple c program as mentioned bellow ... That's bad advice, since Gimpel's product is PC-lint, which has ... to put up with in splint. ...
    (comp.lang.c)
  • Re: Is this wrong or is splint broken?
    ... without complaining no matter how many warnings I enable, ... splint has a parse error on line 103, ... (Use -retvalint to inhibit warning) ...
    (comp.lang.c)