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

Java compilation error when user code defines Get() in a codatatype #4153

Open
robin-aws opened this issue Jun 8, 2023 · 0 comments · May be fixed by #6054
Open

Java compilation error when user code defines Get() in a codatatype #4153

robin-aws opened this issue Jun 8, 2023 · 0 comments · May be fixed by #6054
Assignees
@olivier-aws
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime testing-method: uniform-backend-testing Issues found by ensuring uniform testing across backends

Comments

@robin-aws
Copy link
Member

Dafny version

4.1.0

Code to produce this issue

codatatype NameclashCo = CoCtor(x: int)
{
  method Get() returns (u: int) { return 79; }
}

Command to run and resulting output

% dafny run -t:java src/Scratch.dfy

Dafny program verifier finished with 1 verified, 0 errors
/Users/salkeldr/Documents/GitHub/libraries/src/Scratch-java/_System/NameclashCo.java:27: error: method Get() is already defined in class NameclashCo
  public java.math.BigInteger Get()
                              ^
1 error
Error while compiling Java files. Process exited with exit code 1

What happened?

Compilation always adds the Get() method for resolving the codatatype, but missing a way to avoid colliding with user code.

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

Mac
@robin-aws robin-aws added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label testing-method: uniform-backend-testing Issues found by ensuring uniform testing across backends lang: java Dafny's Java transpiler and its runtime labels Jun 8, 2023
@olivier-aws olivier-aws self-assigned this Jan 15, 2025
@olivier-aws olivier-aws linked a pull request Jan 17, 2025 that will close this issue
Avoid java compilation error when user code defines Get in a codatatype #6054
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@olivier-aws olivier-aws

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime testing-method: uniform-backend-testing Issues found by ensuring uniform testing across backends
Projects
None yet
Milestone
No milestone
2 participants
@robin-aws @olivier-aws