[splint-discuss] detecting infinite loops

[Thomas]

Hello,
I attached a C source-code file with 6 loops (a-f).

Description of the loops:
  a: infinite, i is not modified
  b: infinite, i is not modified
  c: finite, 10 to 1
  d: infinite, starts from 10
  e: infinite, u is unsigned and can not be < 0, integer wrap-around will happen
  f: infinite, i tested, u modified

splint detection:
  a: correct:
     endless_loops.c:9:8: Suspected infinite loop.  No value used in loop test (i)
                             is modified by test or loop body.
       This appears to be an infinite loop. Nothing in the body of the loop or the
       loop test modifies the value of the loop test. Perhaps the specification of a
       function called in the loop body is missing a modification. (Use -infloops to
       inhibit warning)

  b: correct:
     endless_loops.c:15:8: Suspected infinite loop.  No value used in loop test (i)
                              is modified by test or loop body.
       This appears to be an infinite loop. Nothing in the body of the loop or the
       loop test modifies the value of the loop test. Perhaps the specification of a
       function called in the loop body is missing a modification. (Use -infloops to
       inhibit warning)

  c: correct:
     finite loop, nothing special here

  d: incorrect:
     nothing detected here, only the printf() is mentioned

  e: partly correct:
     endless_loops.c:35:14: Comparison of unsigned value involving zero: u < 0
       An unsigned value is used in a comparison with zero in a way that is either a
       bug or confusing. (Use -unsignedcompare to inhibit warning)

  f: incorrect:
     nothing detected here, only the printf() is mentioned


Loop (d) and (f) can be detected easily I think but they are not.

For (e) the comparsion "u < 0" is mentioned correctly but the infinite loop
that results from it is not mentioned. This is a problem if "-unsignedcompare"
is used on the command line, then the code line is not reported anymore.

Are these kind of infinite loops not supported by splint or did I miss a
flag/annotation?

Thanks.

Thomas

-------------- next part --------------
A non-text attachment was scrubbed...
Name: endless_loops.c
Type: text/x-csrc
Size: 416 bytes
Desc: not available
Url : http://www.cs.virginia.edu/pipermail/splint-discuss/attachments/20080514/269c15d5/attachment.bin