fix: Resolution of static functions-by-method (#2023)

dafny-lang · Apr 16, 2022 · 462d7cd · 462d7cd
1 parent 0b07e94
commit 462d7cd
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 3 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -15,6 +15,7 @@
 - fix: Fix induction hypothesis generated for lemmas with a receiver parameter (https://github.com/dafny-lang/dafny/pull/2002)
 - fix: Make verifier understand `(!new)` (https://github.com/dafny-lang/dafny/pull/1935)
 - fix: Fix initialization of non-auto-init in-parameters in C#/JavaScript/Go compilers (https://github.com/dafny-lang/dafny/pull/1935)
+- fix: Resolution of static functions-by-method (https://github.com/dafny-lang/dafny/pull/2023)
 - fix: Export sets did not work with inner modules (https://github.com/dafny-lang/dafny/pull/2025)
 
 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
@@ -2307,7 +2307,7 @@ void RegisterMembers(ModuleDefinition moduleDef, TopLevelDeclWithMembers cl,
             extraMember.InheritVisibility(m, false);
             members.Add(extraName, extraMember);
           } else if (m is Function f && f.ByMethodBody != null) {
-            RegisterByMethod(f);
+            RegisterByMethod(f, cl);
           }
         } else if (m is Constructor && !((Constructor)m).HasName) {
           reporter.Error(MessageSource.Resolver, m, "More than one anonymous constructor");
@@ -2317,10 +2317,9 @@ void RegisterMembers(ModuleDefinition moduleDef, TopLevelDeclWithMembers cl,
       }
     }
 
-    void RegisterByMethod(Function f) {
+    void RegisterByMethod(Function f, TopLevelDeclWithMembers cl) {
       Contract.Requires(f != null && f.ByMethodBody != null);
 
-      var cl = (TopLevelDeclWithMembers)f.EnclosingClass;
       var tok = f.ByMethodTok;
       var resultVar = f.Result ?? new Formal(tok, "#result", f.ResultType, false, false, null);
       var r = Expression.CreateIdentExpr(resultVar);

diff --git a/Test/git-issues/git-issue-2016.dfy b/Test/git-issues/git-issue-2016.dfy
@@ -0,0 +1,12 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module M {
+  datatype D = D() {
+    static function f(): (res: int) {
+      5
+    } by method {
+      return 5;
+    }
+  }
+}
diff --git a/Test/git-issues/git-issue-2016.dfy.expect b/Test/git-issues/git-issue-2016.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors