[splint-discuss] Loops over pointers

[Terry Colligan]

On Tuesday 23 August 2005 02:55 pm, akarl wrote:
> Terry Colligan wrote:
> >   In code like:
> > 
> > // structure type
> > typedef struct node node;
> > struct node
> >     {
> >     /*@null@*/node next;
> 
> You probably mean `/*@null@*/node *next;'.

  I did, indeed.  Thanks for catching this!


> >     int value;
> >     };
> > 
> > node *first;
> > 
> > int look_for_value(int val)
> >     {
> >     node *n;
> >     for (n = first;  n;  n = n->next)
> 
> If you use
> 
>     for (n = first;  n != NULL;  n = n->next)
> 
> Splint will be happy.

  Splint is indeed happy.  However, my client, whom I am
  trying to switch over to splint is not.  This seems to
  them (and to me) like a bug.  One that would require
  lots of changes in their code (and be uglier code, in
  their opinion.)

  Since a naked pointer can be used in if(), while(), etc.,
  and since the documentation alleges that splint works for
  for() as well, isn't this a bug?

  It certainly seems so to us!


> >         {
> >         if (n->value == val)
> >             return 23;
> >         }
> >     return 0;
> >     }
> > 
> >   Why doesn't splint know that the variable 'n' is not null
> >   in the body of the loop?
> > 
> >   If the loop is coded as the equivalent while() loop, splint
> >   seems to understand.
> > 
> >   I get the following output:
> > Splint 3.1.1 --- 21 Aug 2005
> > 
> > test2.c: (in function look_for_value)
> > test2.c:18:14: Arrow access from possibly null pointer n: n->value
> >   A possibly null pointer is dereferenced.  Value is either the result of a
> >   function which may return null (in which case, code should check it is not
> >   null), or a global, parameter or structure field declared with the null
> >   qualifier. (Use -nullderef to inhibit warning)
> >    test2.c:16:30: Storage n may become null

-- 
Terry

Terry Colligan                         terry-splint at tenberry.com