From de0a78a69aac57b2189caf7d8490975f25aea91a Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 19 May 2011 11:53:56 -0700
Subject: Dafny: let verifier, not the resolver, check for missing cases in
 match expressions/statements

---
 Test/dafny0/ControlStructures.dfy | 65 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 65 insertions(+)
 create mode 100644 Test/dafny0/ControlStructures.dfy

(limited to 'Test/dafny0/ControlStructures.dfy')

diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy
new file mode 100644
index 00000000..eed74634
--- /dev/null
+++ b/Test/dafny0/ControlStructures.dfy
@@ -0,0 +1,65 @@
+datatype D = Green | Blue | Red | Purple;
+
+method M0(d: D)
+{
+  match (d) {  // error: two missing cases: Blue and Purple
+    case Green =>
+    case Red =>
+  }
+}
+
+method M1(d: D)
+  requires d != #D.Blue;
+{
+  match (d) {  // error: missing case: Purple
+    case Green =>
+    case Red =>
+  }
+}
+
+method M2(d: D)
+  requires d != #D.Blue && d != #D.Purple;
+{
+  match (d) {
+    case Green =>
+    case Red =>
+  }
+}
+
+method M3(d: D)
+  requires d == #D.Green;
+{
+  if (d != #D.Green) {
+    match (d) {
+      // nothing here
+    }
+  }
+}
+
+method M4(d: D)
+  requires d == #D.Green || d == #D.Red;
+{
+  if (d != #D.Green) {
+    match (d) {  // error: missing case Red
+      // nothing here
+    }
+  }
+}
+
+function F0(d: D): int
+{
+  match (d)  // error: missing cases Red
+  case Purple => 80
+  case Green => 0
+  case Blue => 2
+}
+
+function F1(d: D, x: int): int
+  requires x < 100;
+  requires d == #D.Red ==> x == 200;  // (an impossibility, given the first precondition, so d != Red)
+{
+  match (d)
+  case Purple => 80
+  case Green => 0
+  case Blue => 2
+}
-- 
cgit v1.2.3