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 | 1ef4a8b7e58c8de43dee6a10249a585eed1929f6 (patch) | |
| tree | 1c397c1ac1a48cff11ba2fbda9e37c9101485dc3 /Test/dafny0/Datatypes.dfy | |
| parent | 1df107c2fc6b09b17c2a884c1c2681cd42cf79a5 (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);
|