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.

Sign up for GitHub

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

Jump to bottom

Miscompilation (scope issue) of labels #2576

Closed
cpitclaudel opened this issue Aug 11, 2022 · 0 comments · Fixed by #2973
Closed

Miscompilation (scope issue) of labels #2576

cpitclaudel opened this issue Aug 11, 2022 · 0 comments · Fixed by #2973
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag

Comments

@cpitclaudel
Copy link
Member

Input:

method Main() {
  label l:
    var x := 1;
  print x;
}

Output:

$ Dafny /compileTarget:java /compile:4 bug.dfy

Dafny program verifier finished with 0 verified, 0 errors
Wrote textual form of target program to bug-java/bug.java
Additional target code written to bug-java/_System/nat.java
Additional target code written to bug-java/_System/__default.java
/home/cpitcla/git/dafny/SMT-LIB-transfromer/Src/Bench/Java.Main-java/bug-java/_System/__default.java:16: error: cannot find symbol
    System.out.print(String.valueOf(_0_x));
                                    ^
  symbol:   variable _0_x
  location: class __default
1 error
Error while compiling Java files. Process exited with exit code 1
@cpitclaudel cpitclaudel added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag lang: java Dafny's Java transpiler and its runtime labels Aug 11, 2022
@cpitclaudel cpitclaudel mentioned this issue Aug 18, 2022
Closed
@cpitclaudel cpitclaudel changed the title Miscompilation (scope issue) of labels in Java Miscompilation (scope issue) of labels Sep 2, 2022
@cpitclaudel cpitclaudel removed the lang: java Dafny's Java transpiler and its runtime label Sep 2, 2022
@MikaelMayer MikaelMayer mentioned this issue Nov 2, 2022
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: Labels are no longer compiled in the case of variable declarations dafny-lang/dafny
1 participant
@cpitclaudel