Frama-C Bug Tracking System - Frama-C
View Issue Details
0000102Frama-CPlug-in > jessiepublic2009-05-27 16:342010-07-13 14:01
Frama-C GIT, precise the release id 
0000102: Jessie: struct field's validity
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)

The following annotated code can not be proved by ATPs.

Function f() needs an invariant on global var v :
    //@ global invariant aa: \valid(&v.c);
that should normally be generated automatically.

Function f2() needs a type invariant :
    //@ type invariant Tt(las* l) = \valid(&(l->c)); but this type invariant is visibly not taken into account in the Why generated file (predicate Tt does exist but is not axiomatized).

Source code:

typedef struct { int c; } las;
las v;
//@ requires \valid(p);
void g(int * p);
void f(){ g(&v.c); }
//@ requires \valid(x);
void f2(las * x){ g(&(x->c)); }

Commande line:
frama-c -jessie-analysis -jessie-gui file.c
No tags attached.
related to 0000369closed cmarche Decreases clause 
Issue History
2009-05-27 16:34dparienteNew Issue
2009-06-05 12:31cmarcheAssigned To => cmarche
2009-06-05 12:31cmarcheStatusnew => acknowledged
2009-10-15 10:49cmarcheStatusacknowledged => confirmed
2010-01-14 08:40signolesRelationship addedrelated to 0000369
2010-07-13 14:01borisNote Added: 0001004

2010-07-13 14:01   
The same problem occurs in this code. In function bar, Jessie is unable to verify to validity of the this-pointer to object a.

typedef struct _A {
int x;

typedef struct _B {
A a;

//@ requires \valid(this);
void foo(A* this) {
this->x = 0;

//@ requires \valid(this);
void bar(B* this) {