Index out of bounds in error dialog if more than one schema variable #3156
Comments
|
Julian @jwiesler, I assigned this to you since you authored the commit hat last touched the line that throws the exception. |
|
This (probably) has nothing to do with my changes, if you look at the diff you can see that I only renamed a function. I'll look into it anyways. |
wadoon
added a commit
that referenced
this issue
Jun 7, 2023
* origin/main: adding test case for error messaging remove sonarqube Fix NPE while extracting recoder error position and use existing information better Fix #3156 Fix proof view filter not applied on load
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Description
Something is wrong (since recently) with the error reporting from the taclet instantiation dialogue.
Reproducible
always
Steps to reproduce
bsum{int i;}(0, 4, i * i) = 42bsum_spliton one of the occurrences of the bsum.heap(sic!) in the instantiation for middle.Apply.Observe the error message:
Index 4 out of bounds for length 1KeY should complain that heap is not an integer.
The example has nothing to do with bsums. The point is that the taclet instantation window must have more than one entry and that an input error occurs in one of the lower fields.
Additional information
Stacktrace
``` java.lang.ArrayIndexOutOfBoundsException: Index 4 out of bounds for length 1 at de.uka.ilkd.key.proof.SVInstantiationParserException.getMessage(SVInstantiationParserException.java:37) at de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel.getStatusString(TacletInstantiationModel.java:178) at de.uka.ilkd.key.gui.TacletMatchCompletionDialog$DataTable.editingStopped(TacletMatchCompletionDialog.java:522) at java.desktop/javax.swing.AbstractCellEditor.fireEditingStopped(AbstractCellEditor.java:152) at de.uka.ilkd.key.gui.TacletMatchCompletionDialog$DataTable$InputEditor.fireEditingStopped(TacletMatchCompletionDialog.java:638) at java.desktop/javax.swing.DefaultCellEditor$EditorDelegate.stopCellEditing(DefaultCellEditor.java:375) at java.desktop/javax.swing.DefaultCellEditor.stopCellEditing(DefaultCellEditor.java:234) at de.uka.ilkd.key.gui.TacletMatchCompletionDialog.pushAllInputToModel(TacletMatchCompletionDialog.java:208) at de.uka.ilkd.key.gui.TacletMatchCompletionDialog.pushAllInputToModel(TacletMatchCompletionDialog.java:200) at de.uka.ilkd.key.gui.TacletMatchCompletionDialog$ButtonListener.actionPerformed(TacletMatchCompletionDialog.java:309) at java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1972) ...The text was updated successfully, but these errors were encountered: