[splint-discuss] Loops over pointers

[Terry Colligan]

On Wednesday 24 August 2005 08:19 am, Tommy Pettersson wrote:
> On Wed, Aug 24, 2005 at 03:17:36PM +0200, akarl wrote:
> > By default Splint also complains about statements like
> > 
> >    if (n) { ... }
> > 
> > where n is an int, whereas
> > 
> >    if (n != 0) { ... }
> > 
> > is OK. This behavior can be changed with the predboolint option. Maybe 
> > we are looking for a predboolptr option here.
> 
> The pred-bool-ptr option exists and muffles
> 
>  if (ptr)
> 
> and
> 
>  if (!ptr)
> 
> but it doesn't convince splint that ptr really is or isn't
> NULL for some mysterious reason.  Bug or not, I think it would
> be great if it did so, although thinking won't change splint...

  Actually, the above isn't quite correct -- splint IS convinced
  that ptr really is NULL for if() and while() -- just not for for().

  For example, in:

=============
// test of splint problem

// structure type
typedef struct node node;
struct node
    {
    /*@null@*/node *next;
    int value;
    };

node *first;

/*@-predboolptr@*/
int look_for_value(int val)
    {
    node *n;

	// coded as a for() loop -- splint complains
    for (n = first;  n;  n = n->next)
        {
        if (n->value == val)
            return 23;
        }

	// coded as a while() loop -- splint is happy
	n = first;
	while (n)
		{
        if (n->value == val)
            return 23;
		n = n->next;
		}

	// coded as an if() test -- splint is happy
	n = first;
loop:
	if (n)
		{
        if (n->value == val)
            return 23;
		n = n->next;
		goto loop;
		}

    return 0;
    }
======

  splint complains about the 'n->value' in the for() loop,
  but not in the if() or while() loops:

===========
~/splint$ splint -exportlocal test2.c
Splint 3.1.1 --- 21 Aug 2005

test2.c: (in function look_for_value)
test2.c:21: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:19:30: Storage n may become null

Finished checking --- 1 code warning
==========

  This seems clearly to be a bug.  I have copied splint-bug to
  amend my earlier report of this problem.

-- 
Terry

Terry Colligan                         terry-splint at tenberry.com