From 15755e486cfe715f15ed7e71938d07800a98a7f2 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Thu, 11 Feb 2016 16:08:27 -0800 Subject: Fix issue 134. Wrong variable was used in the loop. --- Source/Dafny/Resolver.cs | 2 +- Test/dafny4/Bug134.dfy | 23 +++++++++++++++++++++++ Test/dafny4/Bug134.dfy.expect | 4 ++++ 3 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 Test/dafny4/Bug134.dfy create mode 100644 Test/dafny4/Bug134.dfy.expect diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index fe31201a..5a63b4e3 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -5057,7 +5057,7 @@ namespace Microsoft.Dafny var dd = (NewtypeDecl)d; if (DafnyOptions.O.IronDafny) { while (dd.ClonedFrom != null) { - dd = (NewtypeDecl)d.ClonedFrom; + dd = (NewtypeDecl)dd.ClonedFrom; } } var caller = context as ICallable; diff --git a/Test/dafny4/Bug134.dfy b/Test/dafny4/Bug134.dfy new file mode 100644 index 00000000..fff6c36a --- /dev/null +++ b/Test/dafny4/Bug134.dfy @@ -0,0 +1,23 @@ +// RUN: %dafny /compile:0 /ironDafny "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module NativeTypes { + newtype{:nativeType "ushort"} uint16 = i:int | 0 <= i < 0x10000 +} + +abstract module AbstractModuleA +{ + import opened NativeTypes + datatype T = T(i:uint16) +} + +abstract module AbstractModuleB +{ + import opened A as AbstractModuleA +} + +abstract module AbstractModuleC +{ + import opened B as AbstractModuleB +} + diff --git a/Test/dafny4/Bug134.dfy.expect b/Test/dafny4/Bug134.dfy.expect new file mode 100644 index 00000000..d5d7ae53 --- /dev/null +++ b/Test/dafny4/Bug134.dfy.expect @@ -0,0 +1,4 @@ +Bug134.dfy(16,20): Warning: "import A as B" has been deprecated; in the new syntax, it is "import A:B" +Bug134.dfy(21,20): Warning: "import A as B" has been deprecated; in the new syntax, it is "import A:B" + +Dafny program verifier finished with 4 verified, 0 errors -- cgit v1.2.3