[splint-discuss] Splint requires buffer size annotation where notnull should be sufficient

[Holger Arnold]

Hello,

given the following code:

  /* T is some type */

  struct list_node {
      struct list_node *next;
      struct list_node *prev;
      T elem;
  };

  void list_forward(struct list_node **pos)
  /*@modifies *pos@*/
  /*@requires notnull *pos@*/
  {
      *pos = (*pos)->next;
  }

splint -strict produces the following warning:

Possible out-of-bounds store: *pos
    Unable to resolve constraint:
    requires maxSet(pos @ ...) >= 0
     needed to satisfy precondition:
    requires maxSet(pos @ ...) >= 0
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)

Possible out-of-bounds read: *pos
    Unable to resolve constraint:
    requires maxRead(pos @ ...) >= 0
     needed to satisfy precondition:
    requires maxRead(pos @ ...) >= 0
  A memory read references memory beyond the allocated storage. (Use
  -boundsread to inhibit warning)

When I replace 'requires notnull *pos' by 'requires maxSet(pos) >= 0
/\ maxRead(pos) >= 0', the warning goes away.  But shouldn't the
'notnull' annotation be sufficient?

Thanks,

--- Holger
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss