--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Validating pointers



Hi everybody!

 

Probably this is a C doubt, but I couldn?t find yet a answer to my question.

 

I?m trying to prove the proof obligations generated by the JESSIE plug-in to
the following C code:

 

typedef struct ast

      {

      unsigned long *d; 

      int top;    

      } AST;

      

typedef struct

{

  AST *a;

} BST;

 

/*@ requires \valid(a) && \valid(*a);

  @ ensures  \valid(*a) &&

  @         \valid_range((*a)->d,0,((*a)->top)-1); 

  @ */

int g(AST **a);

 

 

/*@ requires \valid(e) && \valid(e->a) && \valid(&(e->a)); 

  @ ensures \valid(e->a) && \valid_range(e->a->d,0,(e->a->top)-1);

  @ */ 

void f(BST *e)

{ 

  g(&(e->a)); 

}

 

Function ?f? argument  is a pointer ?e? to a structure BST. Structure BST
has a field ?a?  which points to a structure ?AST?. 

Function ?g? argument is a pointer  ?a?  that is a pointer to a structure
AST.

 

To validate the pre-conditions on ?g?, I have to assume that:

 

\valid(e) && \valid(e->a) && \valid(&(e->a));

 

My question is, why I have to assume \valid(&(e->a)) ?

Assuming just that \valid(e) && \valid(e->a) is not sufficient?

If I assume that e!=NULL && e->a!=NULL, this does not implies that &(e->a)
!= NULL? 

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090701/87ed3eac/attachment.htm