From 74d1631a4724739dbb897c74713f54c4d060e781 Mon Sep 17 00:00:00 2001 From: qunyanm 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/dafny0/Modules0.dfy | 12 ++++++ Test/dafny0/Modules0.dfy.expect | 3 +- Test/dafny4/Bug125.dfy | 82 +++++++++++++++++++++++++++++++++++++++++ Test/dafny4/Bug125.dfy.expect | 2 + 4 files changed, 98 insertions(+), 1 deletion(-) create mode 100644 Test/dafny4/Bug125.dfy create mode 100644 Test/dafny4/Bug125.dfy.expect (limited to 'Test') 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 -- cgit v1.2.3