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