This project is read-only.

Approvals and closed objects in /3 mode

Aug 22, 2011 at 7:02 PM

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 ? 

Aug 23, 2011 at 8:35 AM

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

Aug 23, 2011 at 1:20 PM

Thanks Mark!

Aug 25, 2011 at 9:34 PM

It was a bug. I have fixed it in ba60e0bc6d67