Drodt
commented
6 months ago
## Description
When attempting to automatically prove the accessible clause of the `insert` method, KeY freezes. The terminal shows that it is stuck in a loop of `NullPointerExceptions`.
```java
//@ ghost \locset footprint;
//@ invariant footprint == \set_union(arr[*], this.*);
//@ public invariant (\forall int i; 0 <= i < arr.length; arr[i] >= 0);
private int[] arr;
/*@ public normal_behavior
@ requires 0 <= e;
@ requires e < arr.length;
@ accessible footprint;
@ assignable arr[e];
@ ensures arr[e] == \old(arr[e]) + 1;
@*/
public void insert(int e) {
++arr[e];
}
```
## Reproducible
Always
### Steps to reproduce
> Describe the steps needed to reproduce the issue.
1. Load the class `AccessibleExample`
2. Select the accessible clause of `insert`.
3. Start auto-proof
> What is the expected/actual behavior?
Expected behavior: The proof should succeed. At least a error should be reported in the UI.
Actual: KeY freezes
### Additional information
> Add more details here. In particular: if you have a stacktrace, put it here.
The terminal output:
```
Exception in thread "SIGINT handler" java.lang.NullPointerException: Cannot invoke "de.uka.ilkd.key.java.Expression.visit(de.uka.ilkd.key.java.visitor.Visitor)" because the return value of "org.key_project.util.collection.ImmutableArray.get(int)" is null
at de.uka.ilkd.key.pp.PrettyPrinter.performActionOnCopyAssignment(PrettyPrinter.java:1283)
at de.uka.ilkd.key.java.expression.operator.CopyAssignment.visit(CopyAssignment.java:74)
at de.uka.ilkd.key.pp.PrettyPrinter.performActionOnStatement(PrettyPrinter.java:831)
at de.uka.ilkd.key.pp.PrettyPrinter.printStatementBlock(PrettyPrinter.java:867)
at de.uka.ilkd.key.pp.PrettyPrinter.performActionOnMethodFrame(PrettyPrinter.java:1157)
at de.uka.ilkd.key.java.statement.MethodFrame.visit(MethodFrame.java:264)
at de.uka.ilkd.key.pp.PrettyPrinter.performActionOnStatement(PrettyPrinter.java:831)
at de.uka.ilkd.key.pp.PrettyPrinter.printStatementBlock(PrettyPrinter.java:867)
at de.uka.ilkd.key.pp.PrettyPrinter.performActionOnStatementBlock(PrettyPrinter.java:843)
at de.uka.ilkd.key.java.StatementBlock.visit(StatementBlock.java:222)
at de.uka.ilkd.key.pp.PrettyPrinter.performActionOnStatement(PrettyPrinter.java:831)
at de.uka.ilkd.key.pp.PrettyPrinter.print(PrettyPrinter.java:91)
at de.uka.ilkd.key.pp.LogicPrinter.printSourceElement(LogicPrinter.java:602)
at de.uka.ilkd.key.pp.LogicPrinter.printJavaBlock(LogicPrinter.java:1648)
at de.uka.ilkd.key.pp.LogicPrinter.printModalityTerm(LogicPrinter.java:1686)
at de.uka.ilkd.key.pp.Notation$ModalityNotation.print(Notation.java:182)
at de.uka.ilkd.key.pp.Notation.printContinuingBlock(Notation.java:59)
at de.uka.ilkd.key.pp.LogicPrinter.printTermContinuingBlock(LogicPrinter.java:876)
at de.uka.ilkd.key.pp.LogicPrinter.maybeParens(LogicPrinter.java:1743)
at de.uka.ilkd.key.pp.LogicPrinter.printUpdateApplicationTerm(LogicPrinter.java:1432)
at de.uka.ilkd.key.pp.Notation$UpdateApplicationNotation.print(Notation.java:220)
at de.uka.ilkd.key.pp.LogicPrinter.printTerm(LogicPrinter.java:774)
at de.uka.ilkd.key.pp.LogicPrinter.maybeParens(LogicPrinter.java:1745)
at de.uka.ilkd.key.pp.LogicPrinter.printUpdateApplicationTerm(LogicPrinter.java:1432)
at de.uka.ilkd.key.pp.Notation$UpdateApplicationNotation.print(Notation.java:220)
at de.uka.ilkd.key.pp.LogicPrinter.printTerm(LogicPrinter.java:774)
at de.uka.ilkd.key.pp.LogicPrinter.quickPrintTerm(LogicPrinter.java:162)
at de.uka.ilkd.key.pp.LogicPrinter.quickPrintTerm(LogicPrinter.java:146)
at de.uka.ilkd.key.gui.prooftree.ProofTreeView$ProofRenderer.renderNonLeaf(ProofTreeView.java:1153)
...
```
[issue-3411.zip](https://github.com/KeYProject/key/files/14328660/issue-3411.zip)
---
* Commit: 3a9f3fbf9a1e016f98c056c5229563a154a1551c
mattulbrich