diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-09-08 09:10:30 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-09-08 09:10:30 -0700 |
| commit | e29fb0ac218c4130594e15abd39c1418f48eda69 (patch) | |
| tree | 06ac586ca8792f1c875cfd336dc524efbd05ac0c /Test/dafny0/Datatypes.dfy | |
| parent | 8f96062d049a940fb5bf7cf99475b4b296b2a49b (diff) | |
Dafny: fixed parsing bug with "!in"
Dafny: fixed translation bug with missing match cases (where the constructor has some parameters)
Dafny: fixed translation bug where the program had forward references to members of a datatype
Diffstat (limited to 'Test/dafny0/Datatypes.dfy')
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index 31b3860a..eb527e0d 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -193,3 +193,28 @@ method InjectivityTests(d: XList) assert d == XCons(d.Car, d.Cdr);
}
}
+
+// -------------
+
+method FwdBug(f: Fwd, initialized: bool)
+ requires !f.FwdCons?;
+{
+ match (f) {
+ case FwdNil =>
+ // Syntactically, there is a missing case here, but the verifier checks that this is still cool.
+ // There was once a bug in Dafny, where this had caused an ill-defined Boogie program.
+ }
+ if (!initialized) { // There was once a Dafny parsing bug with this line
+ }
+}
+
+function FwdBugFunction(f: Fwd): bool
+ requires !f.FwdCons?;
+{
+ match f
+ case FwdNil => true
+ // Syntactically, there is a missing case here, but the verifier checks that this is still cool.
+ // There was once a bug in Dafny, where this had caused an ill-defined Boogie program.
+}
+
+datatype Fwd = FwdNil | FwdCons(int, Fwd);
|