My favorites | Sign in
Project Home Wiki Issues Source
READ-ONLY: This project has been archived. For more information see this post.
Search
for
  Advanced search   Search tips   Subscriptions
Issue 66: Sync-or-swim sometimes does not require unpacking when it should
1 person starred this issue and may be notified of changes. Back to list
Status:  Verified
Owner:  nels.bec...@gmail.com
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

Powered by Google Project Hosting