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

Go "continue" miscompilation error #3978

Closed
Dilan-s opened this issue May 9, 2023 · 0 comments · Fixed by #4171
Closed

Go "continue" miscompilation error #3978

Dilan-s opened this issue May 9, 2023 · 0 comments · Fixed by #4171
Labels
invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: golang Dafny's transpiler to Go and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag

Comments

@Dilan-s
Copy link

Dilan-s commented May 9, 2023

Dafny version

4.1.0

Code to produce this issue

method Main() returns ()
{
 for v_int_7 := 3 to 18
 {
  if (false) {
    continue;
  }
  var v_int_93 := 1;
  print v_int_93, "\n";
 }
}

Command to run and resulting output

$ dafny /compile:2 /compileTarget:go t.dfy

Dafny program verifier finished with 1 verified, 0 errors

# command-line-arguments
t-go/src/t.go:49:12: goto C0 jumps over declaration of _1_v__int__93 at t-go/src/t.go:51:9

What happened?

Compiling with a continue within a for loop in Go leads to the message shown above. This error does not occur in any other language. I would expect this program to compile correctly as the continue is wrapped in an if (false) statement and hence all code below the if should be able to be compiled as it would be run.

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

Linux

@Dilan-s Dilan-s added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label May 9, 2023
@fabiomadge fabiomadge added part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag lang: golang Dafny's transpiler to Go and its runtime invalid translated code The compiler generates invalid code, making the the target language infrastructure crash labels May 10, 2023
MikaelMayer added a commit that referenced this issue Jun 12, 2023
MikaelMayer added a commit that referenced this issue Jul 10, 2023
This PR fixes #3978
Our compiler hit the problem stated there:
golang/go#27165
I haven't tested if this problem is fixed in a more recent version of
the Go compiler, but a workaround I found is to wrap the labelled code
with curly braces, so that the goto escape the scope when jumping to the
label, hence Go does not complain anymore about jumping over variable
declaration

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: golang Dafny's transpiler to Go and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants