Dafny generates double returns

[TheGrandmother]

Dafny version

4.2.0

Code to produce this issue

method five() returns (r:int) {
  return 5;
}

Command to run and resulting output

dafny build -t:js test.dfy
Generates:

    static five() {
      let r = _dafny.ZERO;
      r = new BigNumber(5);
      return r;
      return r;
    }

dafny build -t:go test.dfy
Generates:

func (_static *CompanionStruct_Default___) Five() _dafny.Int {
  var r _dafny.Int = _dafny.Zero
  _ = r
  r = _dafny.IntOfInt64(5)
  return r
  return r
}

dafny build -t:py test.dfy
Generates:

class default__:
    def  __init__(self):
        pass

    @staticmethod
    def five():
        r: int = int(0)
        r = 5
        return r
        return r

What happened?

Even though producing double returns isn't necessarily wrong, it is a bit ugly/silly and can cause warnings/errors from linters and other QA tools.

What type of operating system are you experiencing the problem on?

WSL

[stefan-aws]

Thanks for reporting this. I can confirm the behaviour.

[fabiomadge]

The first return is your explicit return, and the second a catch-all which we could omit in this case, but is sometimes needed. Unfortunately it's not always as easy to spot. Take this example:

method LessEqualFive(i: int) returns (r: bool) {
  if i < 5 {
    return false;
  }
  if 5 <= i {
    return true;
  }
}

It also allows omitting the final return, whereas

method LessEqualFive(i: int) returns (r: bool) {
  if i < 5 {
    return false;
  }
  if 5 < i {
    return true;
  }
}

doesn't. The Java compiler implements a crude check, which identifies only top level returns, but helps for your program. It might make sense to improve on the status quo, by putting that functionality into some shared code instead.
In the meantime, I suggest you replace your return 5 by an r := 5.