--- layout: fc_discuss_archives title: Message 104 from Frama-C-discuss on October 2008 ---
Dear All, Just a small question: are type invariants available in the current (humm! precisely of october, 4) version of Jessie? Indeed, these definition and annotation: typedef struct {int c;} las; //@ type invariant Plas(las v) = \valid(&v.c); do not generate any (of the expected) POs (i.e., nothing appears in the context of POs expressing this type invariant). The goal, here, is to get the validity of [p] in function g specification, through the use of this kind of type invariant: typedef struct { int d; } las2; typedef struct lasx { las2 c; } las; extern las v; //@ type invariant Plasx(struct lasx x) = \valid(&x.c.d); //@ requires \valid(p); assigns *p; ensures *p==3; void g(int * p){*p=3;} //@ assigns v.c.d; ensures v.c.d==3; void f(){g(&v.c.d);} Thanks in advance for your answers! Cheers, Dillon Pariente