class Cell
{
  var value:int;
    
  predicate P { acc(value,50) }
    
  function get():int
    requires P;
  {
    unfolding P in value
  }
    
  method boom(x:Cell, y:Cell)
    requires x!=null && y!=null && x.P && y.P;
	ensures x.P && y.P && (x==y ==> x.get()==100) && (x!=y ==> x.get()==old(x.get()));
  {
    if(x==y)
	{
	  unfold x.P; unfold x.P;
	  y.value:=100;
	  fold y.P; fold y.P;
	}
  }
  
  method skip()
    requires P;
	ensures P;
  {}

  // is the bookkeeping correct when calculating the secondary mask?
  // fold happens once on a statically unknown object
  // intermediate calls to skip happen in all examples to create artificial "changes" to the heap,
  // thereby testing framing in the bookkeeping of folds/unfolds
  method foo(z:Cell)
    requires acc(value,50) && value==2 && z!=null && acc(z.value,50);
  {	
	fold z.P;
	call z.skip();
	fold P;
	call boom(this, z);
	assert this!=z ==> unfolding P in value==2;
	assert this==z ==> unfolding P in value==100;
  }
  
  // must fail: give away all permission, even in pieces, and you lose all information about value
  method hoo()
    requires acc(value);
  {
    fold P;
	call skip();
	fold P;
	fork t:=skip();
	call skip ();
	assert unfolding P in value==old(value); // ERROR: should fail
  }
}