diff options
author | Jason Koenig <unknown> | 2011-06-29 17:33:32 -0700 |
---|---|---|
committer | Jason Koenig <unknown> | 2011-06-29 17:33:32 -0700 |
commit | 1cc99aeb12fb2a63d1ef61ac377e5fa889a243e7 (patch) | |
tree | e2857d5903a82d4e69b13695b962cb80c3bb662a | |
parent | 3bb828b02a76167cc8aa25284663f1524e2b929b (diff) |
Made Receiver mutable, as this cannot be linked properly by the parser.
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 7253e866..0b3435e8 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1341,7 +1341,7 @@ namespace Microsoft.Dafny { {
public readonly Type EType;
public readonly List<Expression> ArrayDimensions;
- public readonly CallStmt InitCall; // may be null (and is definitely null for arrays)
+ public CallStmt InitCall; // may be null (and is definitely null for arrays)
public Type Type; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -1576,14 +1576,14 @@ namespace Microsoft.Dafny { public class CallStmt : Statement {
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Receiver != null);
+ //Contract.Invariant(Receiver != null);
Contract.Invariant(MethodName != null);
Contract.Invariant(cce.NonNullElements(Lhs));
Contract.Invariant(cce.NonNullElements(Args));
}
public readonly List<Expression/*!*/>/*!*/ Lhs;
- public readonly Expression/*!*/ Receiver;
+ public Expression/*!*/ Receiver;
public readonly string/*!*/ MethodName;
public readonly List<Expression/*!*/>/*!*/ Args;
public Method Method; // filled in by resolution
@@ -1593,7 +1593,6 @@ namespace Microsoft.Dafny { : base(tok) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(lhs));
- Contract.Requires(receiver != null);
Contract.Requires(methodName != null);
Contract.Requires(cce.NonNullElements(args));
|