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 65: Implications with constraints aren't 'remembered'
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 13, 2009
If a state invariant includes an implication, and none of the fields in 
that implication are touched/modified, we normally get to remember that 
implication, and we can use it to satisfy the packing requirements for that 
same invariant.

However, this doesn't work when the permission in the implication has 
constraints. For example, a permission with a guarantee, (e.g., 
reject_incoming_requests == true -> full(this,PROTOCOL) in STILLOPEN). This 
is because the check to see whether or not we already know this permission 
(which looks in the knownImplications field of the dynamic state logic) 
uses a call to 'contains' which in turn calls 'equals.' 

The result is false because the known implication includes const 
constraints (there exists) and the implication we have to prove includes 
VAR constraints (forall). These two constraints are literally not equal to 
one another.

We need to check that the implication we know SATISFIES the implication we 
need.
May 18, 2009
Project Member #2 nels.bec...@gmail.com
DynamicStateLogic.isKnownImplication(Aliasing, Implication)
May 18, 2009
Project Member #3 nels.bec...@gmail.com
Fixed in r307, at least to the point where the test passes.

In the long run, this may need more work for other types of implications.
Status: Verified

Powered by Google Project Hosting