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

Reserved name in go not escaped #4181

Closed
fabiomadge opened this issue Jun 14, 2023 · 4 comments · Fixed by #4431
Closed

Reserved name in go not escaped #4181

fabiomadge opened this issue Jun 14, 2023 · 4 comments · Fixed by #4431
Assignees
@MikaelMayer
Labels
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

@fabiomadge
Copy link
Collaborator

Dafny version

4.1.0

Code to produce this issue

module C {}

method Main(){
    print "done\n";
}

Command to run and resulting output

No response

What happened?

Compiling the go sources fails.

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 lang: golang Dafny's transpiler to Go and its runtime labels Jun 14, 2023
@MikaelMayer MikaelMayer self-assigned this Aug 17, 2023
MikaelMayer added a commit that referenced this issue Aug 17, 2023
@MikaelMayer
Add test for issue #4181
2e59f5a
@MikaelMayer MikaelMayer mentioned this issue Aug 17, 2023
Merged
keyboardDrummer pushed a commit that referenced this issue Apr 1, 2024
@MikaelMayer
Fix: Reserved module identifiers correctly escaped in GO (#4431)
690f1f2 
This PR fixes #4181
I added the corresponding test.
Basically, module identifiers did not go through IdProtect when
compiling to go, both on the declaration site and import site. This PR
fixes that.

<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>
@fabiomadge
Copy link
Collaborator Author

fabiomadge commented Apr 1, 2024 •
edited
Loading

Other reserved names, like fmt, are still not escaped properly.

@fabiomadge fabiomadge reopened this Apr 1, 2024
@MikaelMayer
Copy link
Member

It seems that you have more tests in reserve than this issue described.
Can you please create a separate issue for other reserved names that are not escaped properly? #4431 fixes only the problem mentioned in this issue.

@fabiomadge
Copy link
Collaborator Author

I just used the shortest example I could find, I don't have a complete list, sorry.

@MikaelMayer MikaelMayer mentioned this issue Apr 1, 2024
Closed
@MikaelMayer
Copy link
Member

Closed in favor of #5283

MikaelMayer added a commit that referenced this issue Apr 3, 2024
@MikaelMayer
Chore: Move tests in the correct directory
8b332bd 
#4181 added two tests but in the wrong directory. This PR fixes it.
@MikaelMayer MikaelMayer mentioned this issue Apr 3, 2024
Merged
MikaelMayer added a commit that referenced this issue Apr 11, 2024
@MikaelMayer
Chore: Move tests in the correct directory (#5290)
a4972f5 
#4181 added two tests but in the wrong directory. This PR fixes it.

### Description
<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->
<!-- Is this a bug fix for an issue visible in the latest release?
Mention this in the PR details and ensure a patch release is considered
-->

### How has this been tested?
<!-- Tests can be added to
`Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to
`Source/*.Test/…` and run with `dotnet 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
Assignees

@MikaelMayer MikaelMayer

Labels
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
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: Reserved module identifiers correctly escaped in GO dafny-lang/dafny
2 participants
@fabiomadge @MikaelMayer