diff options
| author |  Jason Koenig <unknown> | 2012-07-12 18:42:54 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-12 18:42:54 -0700 |
| commit | 4a86f0e78b3bc289bedf69dbe88ddb60ba328bed (patch) | |
| tree | efcbab5e32fb12056a6df57492d26c2cb2173148 /Dafny | |
| parent | d908f24120b5de7028a39f4e22da121bc26f4287 (diff) | |
Dafny: fixed bug in which old locals were not properly forbidden from being modified during refinement
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/RefinementTransformer.cs | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs index da0a733d..18f7cc61 100644 --- a/Dafny/RefinementTransformer.cs +++ b/Dafny/RefinementTransformer.cs @@ -1603,7 +1603,9 @@ namespace Microsoft.Dafny { foreach (var lhs in stmt.Lhss) {
var l = lhs.Resolved;
if (l is IdentifierExpr) {
- if (RefinementToken.IsInherited(l.tok, m) || ((IdentifierExpr)l).Var is Formal) {
+ var ident = (IdentifierExpr)l;
+ Contract.Assert(ident.Var is VarDecl || ident.Var is Formal); // LHS identifier expressions must be locals or out parameters (ie. formals)
+ if ((ident.Var is VarDecl && RefinementToken.IsInherited(((VarDecl)ident.Var).Tok, m)) || ident.Var is Formal) {
// for some reason, formals are not considered to be inherited.
reporter.Error(l.tok, "cannot assign to variable defined previously");
}
|