Non-empty modalities for taclets in .key-files lead to NPE

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

• Mantis: MT-1447

• Submitted on: 2014-05-26 by (at)mkirsten

• Updated: 2014-08-18

• Assigned to: (at)rbubel

Description

When loading a .key or .proof file with additional taclets which include Java code, a NPE is generated.

Steps to reproduce

Load attached file. The error does not occur when "b=a;" is removed.

Additional Information

Exception in thread "AWT-EventQueue-0" java.lang.NullPointerException
        at de.uka.ilkd.key.gui.KeYMediator.getServices(KeYMediator.java:212)
        at de.uka.ilkd.key.gui.WindowUserInterface.taskFinished(WindowUserInterface.java:154)
        at de.uka.ilkd.key.proof.io.ProblemLoader.fireTaskFinished(ProblemLoader.java:82)
        at de.uka.ilkd.key.proof.io.ProblemLoader.access$100(ProblemLoader.java:32)
        at de.uka.ilkd.key.proof.io.ProblemLoader$1.done(ProblemLoader.java:118)
        at javax.swing.SwingWorker$5.run(SwingWorker.java:737)
        at javax.swing.SwingWorker$DoSubmitAccumulativeRunnable.run(SwingWorker.java:832)
        at sun.swing.AccumulativeRunnable.run(AccumulativeRunnable.java:112)
        at javax.swing.SwingWorker$DoSubmitAccumulativeRunnable.actionPerformed(SwingWorker.java:842)
        at javax.swing.Timer.fireActionPerformed(Timer.java:312)
        at javax.swing.Timer$DoPostEvent.run(Timer.java:244)
        at java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:251)
        at java.awt.EventQueue.dispatchEventImpl(EventQueue.java:733)
        at java.awt.EventQueue.access$200(EventQueue.java:103)
        at java.awt.EventQueue$3.run(EventQueue.java:694)
        at java.awt.EventQueue$3.run(EventQueue.java:692)
        at java.security.AccessController.doPrivileged(Native Method)
        at java.security.ProtectionDomain$1.doIntersectionPrivilege(ProtectionDomain.java:76)
        at java.awt.EventQueue.dispatchEvent(EventQueue.java:703)
        at java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:242)
        at java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:161)
        at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:150)
        at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:146)
        at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:138)
        at java.awt.EventDispatchThread.run(EventDispatchThread.java:91)

Files

bla.key

Notes

(at)rbubel at 2014-05-26

Just a short remark:

• there should not be an NPE, but an error message explaining that:

The reason why it does not parse is because the schemavariable sort is \term and therefore b and a cannot be used in programs. In addition when declaring a program schemavariable variable the names must start with a hash symbol for parsing reasons.

(at)grahl at 2014-05-27

The NPE is due to #1446.

(at)rbubel at 2014-05-27

Fixed. NPE is no longer thrown, but error message is not yet beautiful :-)

Problem was that the WindowsUserInterface executed the error handling case in case of a success and the normal behavior in case of an exception

History

• (at)mkirsten -- (NEW_BUG) 2014-05-26

• (at)mkirsten -- (FILE_ADDED) 2014-05-26

• (at)rbubel -- (BUGNOTE_ADDED) 2014-05-26

• (at)grahl -- (BUGNOTE_ADDED) 2014-05-27

• (at)rbubel -- (NORMAL_TYPE) 2014-05-27

• (at)rbubel -- (BUGNOTE_ADDED) 2014-05-27

• (at)rbubel -- (NORMAL_TYPE) 2014-05-27

• (at)rbubel -- (NORMAL_TYPE) 2014-05-27

• (at)rbubel -- (NORMAL_TYPE) 2014-05-27

• (at)grahl -- (NORMAL_TYPE) 2014-08-18

Attributes

• Category: Proof Loading/Saving
• Status: CLOSED
• Severity: MINOR
• OS:
• Target Version:
• Resolution: FIXED
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: aa5fc6227ad2ec538b78f9315bae8c8cdf870587
• Build:
• Tags []
• Labels: ~Proof Loading/Saving ~Bug ~NORMAL
• Version: 2.2

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:54:28.807Z
• updated_at: 2017-05-29T02:54:29.566Z
• closed_at: 2017-05-29T02:54:29.499Z (closed_by: )
• milestone:
• user_notes_count: 0