search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
42 stars 24 forks source link

no_state modifier no longer supported #3452

Open mattulbrich opened 3 months ago

mattulbrich commented 3 months ago

Description

KeY used to have support for a model method modifier no_state indicating that a method must not at all read from the heap.

Now, using no_state makes KeY throw a technical exception which is not even reported in UI.

Reproducible

always

Steps to reproduce

Load the example and try to run the PO for b: A.java.txt

It should load, but crashes with a stacktrace on the CLI.

Additional information

git-bisecting revealed that this bug has been around for many years.

Exception in thread "AWT-EventQueue-0" java.lang.NullPointerException: Cannot invoke "de.uka.ilkd.key.logic.Term.op()" because "term" is null
    at de.uka.ilkd.key.logic.label.OriginTermLabel.canAddLabel(OriginTermLabel.java:198)
    at de.uka.ilkd.key.logic.TermBuilder.addLabelToAllSubs(TermBuilder.java:1654)
    at de.uka.ilkd.key.logic.TermBuilder.addLabelToAllSubs(TermBuilder.java:1685)
    at de.uka.ilkd.key.logic.TermBuilder.addLabelToAllSubs(TermBuilder.java:2302)
    at de.uka.ilkd.key.proof.init.FunctionalOperationContractPO.buildFrameClause(FunctionalOperationContractPO.java:258)
    at de.uka.ilkd.key.proof.init.AbstractOperationPO.createPost(AbstractOperationPO.java:1083)
    at de.uka.ilkd.key.proof.init.AbstractOperationPO.createModelPOTerm(AbstractOperationPO.java:1147)
    at de.uka.ilkd.key.proof.init.AbstractOperationPO.readProblem(AbstractOperationPO.java:404)
    at de.uka.ilkd.key.proof.init.ProblemInitializer.startProver(ProblemInitializer.java:591)
    at de.uka.ilkd.key.gui.ProofManagementDialog.findOrStartProof(ProofManagementDialog.java:478)
    at de.uka.ilkd.key.gui.ProofManagementDialog.lambda$new$5(ProofManagementDialog.java:221)
    at java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1972)
...