| Issue 8: | Can't get field permissions for unique receiver? | |
| 1 person starred this issue and may be notified of changes. | Back to list |
The following program
@States({"OPEN", "CLOSED"})
@ClassStates({@State(name="OPEN", inv="fact == true"),
@State(name="CLOSED", inv="fact == false")})
public class UniqueUnpack {
private boolean fact = true;
@Unique(fieldAccess = true, requires="OPEN", ensures="CLOSED")
void doUnpacking() {
fact = false;
}
}
Should report no errors, as far as I know. Instead, it reports the error,
"Could not bring receiver into post-condition states [CLOSED] due to
insufficient field permissions." Replacing @Unique with @Full works just
fine.
Sep 11, 2008
Project Member
#1
nels.bec...@gmail.com
Status:
Fixed
|