
Hi all,
In the following example everything works fine with /2 but with /3 the last two invariants are inadmissible.
typedef struct A A;
typedef struct A {
int e;
_(group B)
_(ghost _(:B) volatile int ge)
_(invariant :B (\old(\this>\closed) && !\this>\closed) ==> !((A *)\this)>\closed)
_(invariant :B ((A *)\this)>\closed ==> \unchanged(ge)  \inv2((A *)\this))
_(invariant (\this::B)>\closed)
_(invariant e == ge)
} A;
Is there some hack to make them work with /3 ?
Mikhail.



Hi Mikhail,
this might be a triggering problem or even expected to break with the different modeling of typestate in /3  maybe Michal can chime in.
With an explicit backpointer from the group to the containing structure this can be made working:
#include <vcc.h>
typedef struct A {
int e;
_(group B)
_(ghost _(:B) volatile int ge)
_(ghost _(:B) \object x)
_(invariant :B \old(\this>\closed) && !\this>\closed ==> !x>\closed)
_(invariant :B /* not needed: x>\closed ==> */ \unchanged(ge)  \inv2(x))
_(invariant x == \this)
_(invariant (\this::B)>\closed)
_(invariant e == ge)
} A;
// no groups:
struct B {
volatile int ge;
_(ghost \object x)
_(invariant \old(\this>\closed) && !\this>\closed ==> !x>\closed)
_(invariant \unchanged(ge)  \inv2(x))
};
typedef struct C {
int e;
struct B *b;
_(invariant b>\closed && b>x == \this)
_(invariant e == b>ge)
} C;
Cheers, Mark



Thanks Mark!



It was a bug. I have fixed it in ba60e0bc6d67

