diff options
| -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));
|