On Mon, 2012-07-02 14:58:24 +0200, Holger Arnold wrote:
> 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;
> }
>
> [..]
>
> 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?
Hi Holger,
I think the 'notnull' annotation would be the equivalent to 'requires
notnull pos'. That is, 'notnull' would be satisfied, if 'pos' points
to a NULL pointer.
HTH,
Ludolf
--
Bihl+Wiedemann GmbH
Floßwörthstr. 41
68199 Mannheim, Germany
Tel: +49 621 33996-0
Fax: +49 621 3392239
e-mail: [email protected]
website: www.bihl-wiedemann.de
Sitz der Gesellschaft: Mannheim
Geschäftsführer: Jochen Bihl, Bernhard Wiedemann
Amtsgericht Mannheim HRB 5796
_______________________________________________
splint-discuss mailing list
[email protected]
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
