Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Index out of bounds in error dialog if more than one schema variable #3156

Closed
mattulbrich opened this issue Jun 5, 2023 · 2 comments
Closed

Comments

@mattulbrich
Copy link
Member

Description

Something is wrong (since recently) with the error reporting from the taclet instantiation dialogue.

Reproducible

always

Steps to reproduce

  1. Load the Contraposition example
  2. Do a cut on bsum{int i;}(0, 4, i * i) = 42
  3. Apply the rule bsum_split on one of the occurrences of the bsum.
  4. Enter heap (sic!) in the instantiation for middle.
  5. Press Apply.

Observe the error message: Index 4 out of bounds for length 1

KeY 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) ...
</details>


* Commit: 470b0d67e179aefc5995d4bb1c0bcd0da7654cb8
@mattulbrich
Copy link
Member Author

Julian @jwiesler, I assigned this to you since you authored the commit hat last touched the line that throws the exception.

@jwiesler
Copy link
Contributor

jwiesler commented Jun 5, 2023

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.

jwiesler added a commit that referenced this issue Jun 6, 2023
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
Projects
None yet
Development

No branches or pull requests

2 participants