Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Fwd: TR: Pointer problem with nested objects
  • From: dillon.pariente at dassault-aviation.fr (Dillon Pariente)
  • Date: Mon, 12 Jul 2010 14:27:27 +0200
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