diff options
author | 2012-06-13 18:32:05 -0700 | |
---|---|---|
committer | 2012-06-13 18:32:05 -0700 | |
commit | 57ef7564ca7215699ef2d7f52202ec4b9285a23e (patch) | |
tree | f341406515bf8f7398e9a8249ee62a72165bba87 /Dafny/Resolver.cs | |
parent | 7cabbe6e10f11b90df4e4b5f5a3bb1c2253b87c5 (diff) |
Dafny: allow parallel assignments to assign to the same LHS if the RHS match.
Diffstat (limited to 'Dafny/Resolver.cs')
-rw-r--r-- | Dafny/Resolver.cs | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index e013367b..e7cdef5b 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -1898,13 +1898,15 @@ namespace Microsoft.Dafny { var ie = lhs.Resolved as IdentifierExpr;
if (ie != null) {
if (lhsNameSet.ContainsKey(ie.Name)) {
- Error(s, "Duplicate variable in left-hand side of {1} statement: {0}", ie.Name, callRhs != null ? "call" : "assignment");
+ if (callRhs != null)
+ // only allow same LHS in a multiassignment, not a call statement
+ // others (assign such that ":|", etc.) are handled later.
+ Error(s, "Duplicate variable in left-hand side of call statement: {0}", ie.Name);
} else {
lhsNameSet.Add(ie.Name, null);
}
}
}
-
if (update != null) {
// figure out what kind of UpdateStmt this is
if (firstEffectfulRhs == null) {
|