--- layout: fc_discuss_archives title: Message 104 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie: type invariant



Dear All,

Just a small question: are type invariants available in the current 
(humm! precisely of october, 4) version of Jessie?
Indeed, these definition and annotation:
    typedef struct {int c;} las;
    //@ type invariant Plas(las v) = \valid(&v.c);
do not generate any (of the expected) POs (i.e., nothing appears in the 
context of POs expressing this type invariant).

The goal, here, is to get the validity of [p] in function g 
specification, through the use of this kind of type invariant:

    typedef struct { int d; } las2;
    typedef struct lasx { las2 c; } las;
    extern las v;

    //@ type invariant Plasx(struct lasx x) = \valid(&x.c.d);

    //@ requires \valid(p); assigns *p; ensures *p==3;
    void g(int * p){*p=3;}

    //@ assigns v.c.d; ensures v.c.d==3;
    void f(){g(&v.c.d);}

Thanks in advance for your answers!

Cheers,
Dillon Pariente