no_state modifier no longer supported

[mattulbrich]

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)
...

---

• Commit: 9cc569ccced37e242b3a85779f2afdc42b0031ca