summaryrefslogtreecommitdiff
path: root/Test/dafny0
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0')
-rw-r--r--Test/dafny0/ModuleExport.dfy68
-rw-r--r--Test/dafny0/ModuleExport.dfy.expect9
2 files changed, 77 insertions, 0 deletions
diff --git a/Test/dafny0/ModuleExport.dfy b/Test/dafny0/ModuleExport.dfy
new file mode 100644
index 00000000..81fe0ed5
--- /dev/null
+++ b/Test/dafny0/ModuleExport.dfy
@@ -0,0 +1,68 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module A {
+ default export Public { f, h}
+ export E1 { f, g}
+ export E2 extends Public, E1 {T}
+ export Friend extends Public {g, T}
+ export Fruit {Data}
+
+ method h() {}
+ function f(): int { 818 }
+ function g() : int { 819 }
+ function k() : int { 820 }
+
+ class T
+ {
+ static method l() {}
+ }
+
+ datatype Data = Lemon | Kiwi(int)
+
+}
+
+module B {
+ import X = A.Public
+ method m() {
+ X.h(); // OK
+ assert X.f() == 818; // OK
+ assert X.g() == 819; // error
+ assert X.k() == 820; // error
+ X.T.l(); // error
+ }
+}
+
+module C {
+ import X = A.Friend
+ method m() {
+ X.h(); // OK
+ assert X.f() == 818; // OK
+ assert X.g() == 819; // OK
+ assert X.k() == 820; // error
+ X.T.l(); // OK
+ }
+}
+
+module D {
+ import opened A
+ method m() {
+ h(); // OK
+ assert f() == 818; // OK
+ assert g() == 819; // error
+ assert k() == 820; // error
+ }
+}
+
+module E {
+ import opened A.Fruit
+
+ function G(d: Data): int
+ requires d != Data.Lemon
+ {
+ match d
+ case Lemon => G(d)
+ case Kiwi(x) => 7
+ case Orang => 8 // error
+ }
+} \ No newline at end of file
diff --git a/Test/dafny0/ModuleExport.dfy.expect b/Test/dafny0/ModuleExport.dfy.expect
new file mode 100644
index 00000000..c7444bdb
--- /dev/null
+++ b/Test/dafny0/ModuleExport.dfy.expect
@@ -0,0 +1,9 @@
+ModuleExport.dfy(30,11): Error: unresolved identifier: g
+ModuleExport.dfy(31,11): Error: unresolved identifier: k
+ModuleExport.dfy(32,4): Error: unresolved identifier: T
+ModuleExport.dfy(32,7): Error: expected method call, found expression
+ModuleExport.dfy(42,11): Error: unresolved identifier: k
+ModuleExport.dfy(52,9): Error: unresolved identifier: g
+ModuleExport.dfy(53,9): Error: unresolved identifier: k
+ModuleExport.dfy(66,2): Error: member Orang does not exist in datatype Data
+8 resolution/type errors detected in ModuleExport.dfy