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
- Prev by Date: [Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"
- Next by Date: [Frama-c-discuss] frama-c with cygwin
- Previous by thread: [Frama-c-discuss] Frama-C can't detect "Undefined side-effects in expressions"
- Next by thread: [Frama-c-discuss] frama-c with cygwin
- Index(es):