Skip to content

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

@robin-aws

Description

@robin-aws

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

Metadata

Metadata

Assignees

Labels

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labellang: javaDafny's Java transpiler and its runtimetesting-method: uniform-backend-testingIssues found by ensuring uniform testing across backends

Type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions