summaryrefslogtreecommitdiff
path: root/Test/dafny0/Compilation.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Compilation.dfy')
-rw-r--r--Test/dafny0/Compilation.dfy18
1 files changed, 18 insertions, 0 deletions
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index fd445bc0..9c19a404 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -109,3 +109,21 @@ module A1 {
x.m();
}
}
+
+// ----- keyword escapes (once buggy) -----
+
+module M {
+ datatype fixed = A | B
+ function method F(): fixed
+ {
+ A
+ }
+ class public {
+ var private: int;
+ }
+}
+
+method Caller() {
+ var p := new M.public;
+ var x := p.private;
+}