// 7 errors expected

class C {
  var x: int;
  invariant acc(x) && 0 <= x;

  method seq0() returns (r: int)
  {
    r := x;  // error: cannot access this.x here (90)
  }
  method seq1() returns (r: int)
    requires acc(x);
  {
    r := x;
  }
  method seq2() returns (r: int)
    requires rd(x);
  {
    r := x;
  }
  method seq3() returns (r: int)
    requires rd(x);
  {
    r := x;
    x := x + 1;  // error: cannot write to this.x here (184)
  }

  method main0()
  {
    var c := new C;
    c.x := 0;
    share c;
    var t := c.x;  // error: cannot access c.x now (254)
  }
  method main1()
  {
    var c := new C;
    c.x := 2;
    share c;
    acquire c;
    c.x := c.x - 1;
    release c;  // error: monitor invariant might not hold (362)
  }
  method main2()
  {
    var c := new C;
    c.x := 2;
    share c;
    acquire c;
    c.x := c.x + 1;
    release c;  // good!
  }
  method main3()
  {
    var c := new C;
    c.x := 2;
    share c;
    rd acquire c;
    var tmp := c.x + 1;  // fine
    c.x := tmp;  // error: cannot write to c.x here (582)
    rd release c;
  }
  method main4()
  {
    var c := new C;
    c.x := 2;
    share c;
    acquire c;
    c.x := c.x + 1;
    unshare c;
    c.x := c.x + 1;
  }
  method main5()
  {
    var c := new C;
    unshare c;  // error: cannot unshare an object that isn't shared (754)
  }
  method main6()
  {
    var c := new C;
    c.x := 0;
    share c;  acquire c;
    unshare c;
    unshare c;  // error: cannot unshare an object that isn't shared (862)
  }
}