diff options
| author |  qunyanm <unknown> | 2016-03-21 11:45:14 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2016-03-21 11:45:14 -0700 |
| commit | a89b9aee05dff74345a79f8fb4fe0fe3fdbb17ad (patch) | |
| tree | 251401e34f6ddbc73623e63f3f6d6637b2d0d088 /Test | |
| parent | acbc126c01fee3ab71647a7b16f4dcfc80eee2ea (diff) | |
Update module export error messages. Also for "import Y" if there is at least
one exported view, but no exported view is marked as default, then it is an
error.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/ModuleExport.dfy | 37 | ||||
| -rw-r--r-- | Test/dafny0/ModuleExport.dfy.expect | 6 |
2 files changed, 42 insertions, 1 deletions
diff --git a/Test/dafny0/ModuleExport.dfy b/Test/dafny0/ModuleExport.dfy index 81fe0ed5..1e69764f 100644 --- a/Test/dafny0/ModuleExport.dfy +++ b/Test/dafny0/ModuleExport.dfy @@ -65,4 +65,41 @@ module E { case Kiwi(x) => 7
case Orang => 8 // error
}
+}
+
+module F {
+ default export Public { f, h}
+ default export E1 { f, g}
+ export E2 extends Public2, E1 {T} // error: Public2 is not a exported view of F
+ export Friend extends Public {g2, T} // error: g2 is not a member of F
+ 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 G {
+ export Public { f, h}
+
+ method h() {}
+ function f(): int { 818 }
+ function g() : int { 819 }
+ function k() : int { 820 }
+}
+
+module H {
+ import G // error: G has no default export
+}
+
+module I {
+ import G.Public // OK
}
\ No newline at end of file diff --git a/Test/dafny0/ModuleExport.dfy.expect b/Test/dafny0/ModuleExport.dfy.expect index c7444bdb..274c8f31 100644 --- a/Test/dafny0/ModuleExport.dfy.expect +++ b/Test/dafny0/ModuleExport.dfy.expect @@ -6,4 +6,8 @@ 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
+ModuleExport.dfy(70,7): Error: Public2 must be an export of F to be extended
+ModuleExport.dfy(74,9): Error: g2 must be a member of F to be exported
+ModuleExport.dfy(70,7): Error: more than one default export declared in module F
+ModuleExport.dfy(90,7): Error: no default export declared in module: G
+12 resolution/type errors detected in ModuleExport.dfy
|