Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dafny generates invalid Java code #1297

Open
sorawee opened this issue Jul 13, 2021 · 0 comments
Open

Dafny generates invalid Java code #1297

sorawee opened this issue Jul 13, 2021 · 0 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime

Comments

@sorawee
Copy link
Contributor

sorawee commented Jul 13, 2021

method Main () 
{
  var x := 0;
  var z := (
    var y := 0;
    x
  );
}

generates the following Java code:

  public static void Main()
  {
    java.math.BigInteger _13_x = java.math.BigInteger.ZERO;
    _13_x = java.math.BigInteger.ZERO;
    java.math.BigInteger _14_z = java.math.BigInteger.ZERO;
    _14_z = dafny.Helpers.<java.math.BigInteger, java.math.BigInteger>Let(java.math.BigInteger.ZERO, _pat_let0_0 -> dafny.Helpers.<java.math.BigInteger, java.math.BigInteger>Let(_pat_let0_0, _15_y -> _13_x));
  }

which errors:

_System/__default.java:15: error: local variables referenced from a lambda expression must be final or effectively final
@keyboardDrummer keyboardDrummer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime labels Jul 13, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime
Projects
None yet
Development

No branches or pull requests

2 participants