diff options
| author |  Rustan Leino <unknown> | 2013-06-25 15:32:39 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-06-25 15:32:39 -0700 |
| commit | d55819f900ea34132987eb8aa1e9990dce96729b (patch) | |
| tree | 4e1de152e3ae3b576f53fa9094bc4ce69c9bab24 /Test/dafny0/Compilation.dfy | |
| parent | 6f8d64477512d93bb127c7cd9b9134840dabe4da (diff) | |
Fixed compilation bug where C# keywords were not being escaped
Diffstat (limited to 'Test/dafny0/Compilation.dfy')
| -rw-r--r-- | Test/dafny0/Compilation.dfy | 18 |
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;
+}
|