Inifite NullPointerExceptions when proving accessible clause

[Drodt]

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.

//@ 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

• Commit: 3a9f3fb

[mattulbrich]

mmmh. Accessible clauses for void methods do not make sense in the sense in which KeY interprets the annotation. However, this is absolultely no reason to get stuck.

[Drodt]

mmmh. Accessible clauses for void methods do not make sense in the sense in which KeY interprets the annotation. However, this is absolultely no reason to get stuck.

Right, I forgot about that. Still, this specific error is unexpected. I also do not know why pretty printing only fails for accessible clauses.