diff options
author | 2011-05-19 11:53:56 -0700 | |
---|---|---|
committer | 2011-05-19 11:53:56 -0700 | |
commit | de0a78a69aac57b2189caf7d8490975f25aea91a (patch) | |
tree | c94831db7e3d99c333afe55d5d586b8147dace31 /Source/Dafny/DafnyAst.cs | |
parent | b665a914c81085cf3ac4e97ea3c73673cfe8ca4b (diff) |
Dafny: let verifier, not the resolver, check for missing cases in match expressions/statements
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index d83560e0..04d92539 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1642,10 +1642,12 @@ namespace Microsoft.Dafny { void ObjectInvariant() {
Contract.Invariant(Source != null);
Contract.Invariant(cce.NonNullElements(Cases));
+ Contract.Invariant(cce.NonNullElements(MissingCases));
}
public readonly Expression Source;
public readonly List<MatchCaseStmt/*!*/>/*!*/ Cases;
+ public readonly List<DatatypeCtor/*!*/> MissingCases = new List<DatatypeCtor>(); // filled in during resolution
public MatchStmt(IToken tok, Expression source, [Captured] List<MatchCaseStmt/*!*/>/*!*/ cases)
: base(tok) {
@@ -2490,10 +2492,13 @@ namespace Microsoft.Dafny { public class MatchExpr : Expression { // a MatchExpr is an "extended expression" and is only allowed in certain places
public readonly Expression Source;
public readonly List<MatchCaseExpr/*!*/>/*!*/ Cases;
+ public readonly List<DatatypeCtor/*!*/> MissingCases = new List<DatatypeCtor>(); // filled in during resolution
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Source != null);
Contract.Invariant(cce.NonNullElements(Cases));
+ Contract.Invariant(cce.NonNullElements(MissingCases));
}
public MatchExpr(IToken tok, Expression source, [Captured] List<MatchCaseExpr/*!*/>/*!*/ cases)
|