Issue 66: Sync-or-swim sometimes does not require unpacking when it should
Status:  Verified
Owner:
Closed:  May 2009
Project Member Reported by nels.bec...@gmail.com, May 20, 2009
In this method of the Blocking_queue, sync-or-swim does not require 
unpacking even though I believe it should:
@Pures({
  @Pure(guarantee="PROTOCOL", requires="STILLOPEN", ensures="STILLOPEN"),
  @Pure(guarantee="STRUCTURE", use=Use.FIELDS)
})
public final boolean is_empty()
{	
  return elements.size() <= 0; }
}

Instead what happens is that it forgets 'this' and the error is that 'this' 
is not in the required state on return. This is a big problem and I think I 
noticed this in NIMBY as well.


May 20, 2009
Project Member #1 nels.bec...@gmail.com
Fixed in r308.
Status: Verified