diff options
author | 2011-04-05 17:03:28 -0700 | |
---|---|---|
committer | 2011-04-05 17:03:28 -0700 | |
commit | 343f29bee9cad726c2de33d4ef6cdb49caa965d2 (patch) | |
tree | bc40127c4275c0a91c42620f5b4a6d96b5f61871 /Source/Dafny/DafnyAst.cs | |
parent | 2b09756f836307f75a36c5a982784dc620fda657 (diff) |
Dafny: Allow field selections and array-element selection as LHSs of assignments where RHS is not just an expression
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index d168e519..045f879a 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1294,6 +1294,7 @@ namespace Microsoft.Dafny { public abstract class AssignmentRhs {
internal AssignmentRhs() {
}
+ public abstract bool CanAffectPreviouslyKnownExpressions { get; }
}
public abstract class DeterminedAssignmentRhs : AssignmentRhs {
@@ -1312,6 +1313,7 @@ namespace Microsoft.Dafny { Contract.Requires(expr != null);
Expr = expr;
}
+ public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }
}
public class TypeRhs : DeterminedAssignmentRhs {
@@ -1341,9 +1343,22 @@ namespace Microsoft.Dafny { EType = type;
ArrayDimensions = arrayDimensions;
}
+ public override bool CanAffectPreviouslyKnownExpressions {
+ get {
+ if (InitCall != null) {
+ foreach (var mod in InitCall.Method.Mod) {
+ if (!(mod.E is ThisExpr)) {
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+ }
}
public class HavocRhs : AssignmentRhs {
+ public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }
}
public class AssignStmt : Statement {
|