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 | c71f8edce17944b5198ac968da17c19c96b39877 (patch) | |
| tree | afb3ae33425416064369f8c93ab5bbc798cf2d39 /Source | |
| parent | 2ee898b3b9c55b8347182562b8b0a92aeda223e1 (diff) | |
Dafny: fixed bug in which old locals were not properly forbidden from being modified during refinement
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index da0a733d..18f7cc61 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/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");
}
|