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 10: Tell user if there are parse errors in permission annotations!
1 person starred this issue and may be notified of changes. Back to list
Status:  Fixed
Owner:  nels.bec...@gmail.com
Closed:  Sep 2008


 
Project Member Reported by nels.bec...@gmail.com, Sep 15, 2008
We need to somehow tell the user if there are parse errors in permission 
annotations. Otherwise, you can be lead on a wild goose chase! Here's a 
good example:

@Perm(requires="full(this)", ensures="full(result")
PostTest m2() {
return this;
}

PLURAL tells us nothing about the parse error in the ensures clause. 
However, this causes the result permission (which we must prove) to be:

[] frame [] with Nil

This is crazy.
Sep 16, 2008
Project Member #1 nels.bec...@gmail.com
This is fixed in revision 45 for @Perm and @State annotations. Are there any that I 
missed?
Status: Fixed

Powered by Google Project Hosting