diff options
Diffstat (limited to 'Test')
-rw-r--r-- | Test/dafny0/Modules0.dfy | 12 | ||||
-rw-r--r-- | Test/dafny0/Modules0.dfy.expect | 3 | ||||
-rw-r--r-- | Test/dafny4/Bug125.dfy | 82 | ||||
-rw-r--r-- | Test/dafny4/Bug125.dfy.expect | 2 |
4 files changed, 98 insertions, 1 deletions
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index dbbffd87..4b86d848 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -335,3 +335,15 @@ module TopLevelStatics { static method M() // error/warning: static keyword does not belong here
{ }
}
+
+module Library {
+ class T { }
+}
+
+module AA {
+ import opened Library
+}
+
+module B refines AA {
+ datatype T = MakeT(int) // illegal
+}
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index e4b46cce..f51e0f6c 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -30,5 +30,6 @@ Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'
Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
Modules0.dfy(324,30): Error: member Create does not exist in class Klassy
+Modules0.dfy(348,11): Error: a datatype declaration (T) in a refinement module can only replace an opaque type declaration
Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name or declare a module import 'opened?')
-31 resolution/type errors detected in Modules0.dfy
+32 resolution/type errors detected in Modules0.dfy
diff --git a/Test/dafny4/Bug125.dfy b/Test/dafny4/Bug125.dfy new file mode 100644 index 00000000..916dd3f8 --- /dev/null +++ b/Test/dafny4/Bug125.dfy @@ -0,0 +1,82 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module AbstractModuleA
+{
+ type T
+}
+
+abstract module AbstractModuleB
+{
+ import opened AMA : AbstractModuleA
+
+ method Foo(t:T)
+}
+
+abstract module AbstractModuleC refines AbstractModuleB
+{
+ import opened AMA2 : AbstractModuleA
+}
+
+module LibA {
+ class G {
+ static function f(x:int) : bool {
+ x >= 10
+ }
+ }
+
+ function g() : bool {
+ true
+ }
+}
+
+module LibB {
+ class G {
+ static function f(x:int) : bool {
+ x < 10
+ }
+ }
+
+ function g() : bool {
+ false
+ }
+}
+
+module R {
+ import opened LibA
+}
+
+module S refines R {
+ import opened LibB
+ method m() {
+ assert g(); // should be LibA.g
+ }
+
+ method m1() {
+ assert G.f(20); // should be LibA.G.f
+ }
+}
+
+
+module Library {
+
+ class T { }
+
+}
+
+
+
+module A {
+
+ import opened Library
+ class T {
+ }
+}
+
+
+
+module B refines A {
+
+ datatype T = MakeT(int) // illegal for the same reason as above, but Dafny fails to issue an error
+
+}
diff --git a/Test/dafny4/Bug125.dfy.expect b/Test/dafny4/Bug125.dfy.expect new file mode 100644 index 00000000..c87e2af2 --- /dev/null +++ b/Test/dafny4/Bug125.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 10 verified, 0 errors
|