Skip to content

Dafny uses incorrect accessor names for Java interfaces #6425

@fcseidl

Description

@fcseidl

Dafny version

4.11.0

Code to produce this issue

In AccessorNames.dfy, declare an external Java interface, and a method which sets a property of that interface:

module {:compile false} {:extern} SomePkg {
    trait SomeInterface {
        var myBool: bool
    }
}

module {:extern} M {
    import opened SomePkg

    class C {
        static method MakeItTrue(someObj: SomeInterface)
            modifies someObj
            ensures someObj.myBool
        {
            someObj.myBool := true;
        }
    }
}

Command to run and resulting output

Run dafny translate java AccessorNames.dfy. Then, AccessorNames-java/M/C.java reads:

// Class C
// Dafny class C compiled into Java
package M;

@SuppressWarnings({"unchecked", "deprecation"})
public class C {
  public C() {
  }
  public static void MakeItTrue(SomePkg.SomeInterface someObj)
  {
    (someObj).set_myBool(true);
  }
  @Override
  public java.lang.String toString() {
    return "M.C";
  }
}

What happened?

Dafny makes an unfounded assumption about how the external setter method is named. If SomeInterface.set_myBool existed and behaved as Dafny expects, this wouldn't be a problem. But the codebase I am working with uses JavaBeans conventions, by which the setter is called setMyBool. As such, set_myBool is an undefined symbol and compilation fails.

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions