--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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