Cannot parse constructor that accepts varargs

[FliegendeWurst]

Description

KeY fails to load a .java file where a constructor accepts a variable number of arguments.

Reproducible

always

Steps to reproduce

Load Varargs.java, try to prove the constructor contract:

class Varargs {
    /*@ public normal_behavior
      @ ensures this != null;
      @*/
    public Varargs(int... inp) {
    }
}

Expected behavior: it works
Actual behavior: it fails to load with an exception

Additional information

Stacktrace

Assertion failure: Call to non-existent constructor.
	at de.uka.ilkd.key.util.Debug.fail(Debug.java:105)
	at de.uka.ilkd.key.util.Debug.assertTrue(Debug.java:55)
	at de.uka.ilkd.key.rule.metaconstruct.ConstructorCall.constructorCallSequence(ConstructorCall.java:151)
	at de.uka.ilkd.key.rule.metaconstruct.ConstructorCall.transform(ConstructorCall.java:102)
	at de.uka.ilkd.key.proof.init.FunctionalOperationContractPO.buildOperationBlocks(FunctionalOperationContractPO.java:159)
	at de.uka.ilkd.key.proof.init.AbstractOperationPO.createNonModelPOTerm(AbstractOperationPO.java:1124)
	at de.uka.ilkd.key.proof.init.AbstractOperationPO.readProblem(AbstractOperationPO.java:438)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.startProver(ProblemInitializer.java:580)
	at de.uka.ilkd.key.gui.ProofManagementDialog.findOrStartProof(ProofManagementDialog.java:476)
	at de.uka.ilkd.key.gui.ProofManagementDialog.lambda$new$5(ProofManagementDialog.java:220)

---

• Commit: 7750e75

[WolframPfeifer]

Although I could not find any explicit reference, I don't think that we support varargs in general. I agree that there should be a more helpful error message.

For the moment, a workaround would be to rewrite the constructor to accept an int array (although this adds a bit of boilerplate), which is what happens implicitly.