Skip to content

Can't save proof with long package name as proof bundle #3677

@FliegendeWurst

Description

@FliegendeWurst

Description

If a proof name contains very long package names, it can't be saved as a proof bundle (.zproof).

Reproducible

always

Steps to reproduce

  1. Load and prove the method below
  2. Try to save as proof bundle
package very.large.path.with.lots.of.members;

class LongMethodName {
    /*@ public normal_behaviour
      @ ensures \result == 100;
      @*/
    public int doIt(LongMethodName a, LongMethodName b, LongMethodName c) {
        return 100;
    }
}

Expected behaviour: it works
Actual behaviour: it fails with an exception

Additional information

[15:45:17.768] WARN  ProofSaver - Failed to save java.io.FileNotFoundException: /tmp/KeYTmpFileRepo15620876094854547731/very.large.path.with.lots.of.members.LongMethodName(very.large.path.with.lots.of.members.LongMethodName__doIt(very.large.path.with.lots.of.members.LongMethodName,very.large.path.with.lots.of.members.LongMethodName,very.large.path.with.lots.of.members.LongMethodName)).JML normal_behavior operation contract.0.proof (File name too long)
        at java.base/java.io.FileOutputStream.open0(Native Method)
        at java.base/java.io.FileOutputStream.open(FileOutputStream.java:289)
        at java.base/java.io.FileOutputStream.<init>(FileOutputStream.java:230)
        at java.base/java.io.FileOutputStream.<init>(FileOutputStream.java:179)
        at de.uka.ilkd.key.proof.io.consistency.DiskFileRepo.createOutputStream(DiskFileRepo.java:271)
        at de.uka.ilkd.key.proof.io.ProofBundleSaver.save(ProofBundleSaver.java:57)
        at de.uka.ilkd.key.proof.io.ProofSaver.save(ProofSaver.java:127)
        at de.uka.ilkd.key.gui.WindowUserInterfaceControl.saveProofBundle(WindowUserInterfaceControl.java:430)
        at de.uka.ilkd.key.gui.actions.ShowProofStatistics$Window.lambda$init$4(ShowProofStatistics.java:311)
        at java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1972)

  • Commit: ec5929d (on JML proof scripts branch, but the issue occurs on main as well)

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions