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

[Frama-c-discuss] Fwd: TR: Pointer problem with nested objects



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