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] Pointer problem with nested objects

  • Subject: [Frama-c-discuss] Pointer problem with nested objects
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Sat, 10 Jul 2010 13:12:16 +0200
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