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

Second assignment to const crashes the Rust compiler #5642

Closed
Tracked by #5561
fabiomadge opened this issue Jul 22, 2024 · 0 comments · Fixed by #5667
Closed
Tracked by #5561

Second assignment to const crashes the Rust compiler #5642

fabiomadge opened this issue Jul 22, 2024 · 0 comments · Fixed by #5667
Labels
during 2: compilation of correct program Dafny rejects a valid program during compilation has-workaround: yes There is a known workaround kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: rust Dafny's transpiler to Rust and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag

Comments

@fabiomadge
Copy link
Collaborator

Dafny version

4.7.0

Code to produce this issue

class Cl {
  const c: bool
  constructor(c: bool) {
    this.c := c;
    this.c := c;
  }
}

method Main() {
  var cl := new Cl(false);
  print cl.c, "\n";
}

Command to run and resulting output

No response

What happened?

This shouldn't crash

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

Mac

@fabiomadge fabiomadge 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 has-workaround: yes There is a known workaround during 2: compilation of correct program Dafny rejects a valid program during compilation lang: rust Dafny's transpiler to Rust and its runtime labels Jul 22, 2024
MikaelMayer added a commit that referenced this issue Sep 6, 2024
This PR fixes #5642
I added the corresponding test.

<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
during 2: compilation of correct program Dafny rejects a valid program during compilation has-workaround: yes There is a known workaround kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: rust Dafny's transpiler to Rust 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.

1 participant