diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-19 11:53:56 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-19 11:53:56 -0700 |
| commit | de0a78a69aac57b2189caf7d8490975f25aea91a (patch) | |
| tree | c94831db7e3d99c333afe55d5d586b8147dace31 /Test/dafny0 | |
| parent | b665a914c81085cf3ac4e97ea3c73673cfe8ca4b (diff) | |
Dafny: let verifier, not the resolver, check for missing cases in match expressions/statements
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 36 | ||||
| -rw-r--r-- | Test/dafny0/ControlStructures.dfy | 65 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
3 files changed, 102 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 34aea30b..28f438af 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -540,6 +540,42 @@ Execution trace: Dafny program verifier finished with 6 verified, 1 error
+-------------------- ControlStructures.dfy --------------------
+ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
+Execution trace:
+ (0,0): anon0
+ (0,0): anon6_Else
+ (0,0): anon7_Else
+ (0,0): anon8_Else
+ (0,0): anon9_Then
+ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
+Execution trace:
+ (0,0): anon0
+ (0,0): anon6_Else
+ (0,0): anon7_Else
+ (0,0): anon8_Then
+ControlStructures.dfy(14,3): Error: missing case in case statement: Purple
+Execution trace:
+ (0,0): anon0
+ (0,0): anon6_Else
+ (0,0): anon7_Else
+ (0,0): anon8_Then
+ControlStructures.dfy(43,5): Error: missing case in case statement: Red
+Execution trace:
+ (0,0): anon0
+ (0,0): anon8_Then
+ (0,0): anon9_Else
+ (0,0): anon10_Then
+ControlStructures.dfy(51,3): Error: missing case in case statement: Red
+Execution trace:
+ (0,0): anon8_Else
+ (0,0): anon9_Else
+ (0,0): anon10_Else
+ (0,0): anon11_Else
+ (0,0): anon12_Then
+
+Dafny program verifier finished with 8 verified, 5 errors
+
-------------------- Termination.dfy --------------------
Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
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
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index f67429d2..16bc0e2b 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -15,7 +15,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.dfy ResolutionErrors.dfy
Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy
Modules0.dfy Modules1.dfy BadFunction.dfy
- Comprehensions.dfy
+ Comprehensions.dfy ControlStructures.dfy
Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
Refinement.dfy RefinementErrors.dfy) do (
|