--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on February 2011 ---
Hello, this code doesn't verify with Jessie: typedef struct { int v; } A; typedef struct { A a; } B; //@ requires \valid(this); void bar(A* this); //@ requires \valid(this); void foo(B* this) { bar(&this->a); // call doesn't verify } Why does the precondition \valid(this) in foo not imply \valid(&this->a)? Shouldn't pointer b of type B be valid iff the span of b is valid? -- Regards, Boris