From 74d1631a4724739dbb897c74713f54c4d060e781 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Fri, 5 Feb 2016 15:18:29 -0800
Subject: Fix issue 125. Add the missing case 2 and 3 with refinement and
 opened imports. For the following situation  module LibA {  // ...things
 declared here...  }
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

 module LibB {
 // ...things declared here...
 }

 module R {
 import opened LibA
 // ...things declared here...
 }

 module S refines R {
 import opened LibB
 // ...declared here...
 }

 1. If module R declares a TopLevelDecl “G”, then we should report an error if S
 attempts to declare an incompatible TopLevelDecl “G”. Dafny does this already.

 2. If LibA declares a TopLevelDecl “G” but R does not directly declare any
 TopLevelDecl G”, then we should also issue an error for any TopLevelDecl “G”
 in S. This behavior is missing in Dafny.

 3. If each of LibA and LibB declares some TopLevelDecl “G”, but neither R nor S
 directly declares any TopLevelDecl “G”, then no error should be issued, and
 any use of “G” in S should resolve to the “G” in LibA. This behavior is missing
 in Dafny.
---
 Test/dafny4/Bug125.dfy | 82 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 82 insertions(+)
 create mode 100644 Test/dafny4/Bug125.dfy

(limited to 'Test/dafny4/Bug125.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
+
+}
-- 
cgit v1.2.3


From 6ea62e3009f326ca553521c169dec67a262a7217 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Fri, 5 Feb 2016 18:09:23 -0800
Subject: Last checkin checked in the wrong version of bug125.dfy. The failure
 part of the test was moved into test\dafny0\modules0.dfy so that bug125.dfy
 can be verified that it was resolved to the correct types.

---
 Test/dafny4/Bug125.dfy | 24 ------------------------
 1 file changed, 24 deletions(-)

(limited to 'Test/dafny4/Bug125.dfy')

diff --git a/Test/dafny4/Bug125.dfy b/Test/dafny4/Bug125.dfy
index 916dd3f8..5dbdea6f 100644
--- a/Test/dafny4/Bug125.dfy
+++ b/Test/dafny4/Bug125.dfy
@@ -56,27 +56,3 @@ module S refines R {
    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
-
-}
-- 
cgit v1.2.3