--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on July 2010 ---
This seems to be in the scope of http://bts.frama-c.com/view.php?id=102. One can (temporarily?) get around this by writing: //@ requires \valid(this) && \valid(&this->a); HTH D. -----Message d'origine----- De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Boris Hollas Envoy? : samedi 10 juillet 2010 13:12 ? : Frama-C public discussion Objet : [Frama-c-discuss] Pointer problem with nested objects Hi, in this code I have an object that contains another object as a delegate: typedef struct _A { int x; }A; typedef struct _B { A a; }B; //@ requires \valid(this); void foo(A* this) { this->x = 0; } //@ requires \valid(this); void bar(B* this) { foo(&this->a); } In function bar, Jessie is unable to verify offset_min(_A_this_0_2_alloc_table, result) <= 0 offset_max(_A_this_0_2_alloc_table, result) >= 0 for { (C_8 : foo((C_7 : this_0.a))); I don't know what this means, but it must have to do with the validity of the pointer to object A. However, this pointer should be valid because the pointer to B is valid. What is wrong here? -- Regards, Boris