fix: Don’t entirely delete by-method part in export scope checks (#1855)

RELEASE_NOTES.md

@@ -3,6 +3,7 @@
 - feat: `continue` statements. Like Dafny's `break` statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section [19.2](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-break-continue) of the Reference Manual. (https://github.com/dafny-lang/dafny/pull/1839)
 - feat: The keyword syntax for functions will change in Dafny version 4. The new command-line option `/functionSyntax` (see `/help`) allows early adoption of the new syntax. (https://github.com/dafny-lang/dafny/pull/1832)
 - fix: No warning "File contains no code" if a file only contains a submodule (https://github.com/dafny-lang/dafny/pull/1840)
+- fix: export-reveals of function-by-method now allows the function body to be ghost (https://github.com/dafny-lang/dafny/pull/1855)
 
 
 # 3.4.2

Source/Dafny/Cloner.cs

@@ -974,9 +974,18 @@ public override Field CloneField(Field f) {
 
  public override Function CloneFunction(Function f, string newName = null) {
  var basef = base.CloneFunction(f, newName);
- basef.ByMethodTok = null; // never export the method body of a function-by-method
- basef.ByMethodBody = null; // never export the method body of a function-by-method
- Contract.Assert(basef.ByMethodDecl == null);
+ if (basef.ByMethodBody != null) {
+ Contract.Assert(!basef.IsGhost); // a function-by-method has .IsGhost == false
+ Contract.Assert(basef.Body != null); // a function-by-method has a nonempty .Body
+ if (RevealedInScope(f)) {
+ // For an "export reveals", use an empty (but not absent) by-method part.
+ basef.ByMethodBody = new BlockStmt(basef.ByMethodBody.Tok, basef.ByMethodBody.EndTok, new List<Statement>());
+ } else {
+ // For an "export provides", remove the by-method part altogether.
+ basef.ByMethodTok = null;
+ basef.ByMethodBody = null;
+ }
+ }
  if (!RevealedInScope(f)) {
  basef.Body = null;
  }

Test/git-issues/git-issue-1852.dfy

@@ -0,0 +1,38 @@
+// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module A {
+ export
+ reveals F, G
+
+ function G(): int { 5 }
+
+ function F(): int {
+ G()
+ } by method {
+ return 5;
+ }
+}
+
+module B {
+ export
+ provides F
+
+ function G(): int { 5 }
+
+ function F(): int {
+ G()
+ } by method {
+ return 5;
+ }
+}
+
+module Client {
+ import A
+ import B
+
+ method Main() {
+ // Test that A.F and B.F are both non-ghost here
+ print A.F(), " ", B.F(), "\n"; // 5 5
+ }
+}

Test/git-issues/git-issue-1852.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 4 verified, 0 errors
+5 5