| 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 |
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
Status:
Fixed
|