--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on July 2009 ---
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