key Exception while saving proofs

Exception while saving proofs

Open wadoon opened this issue 2 years ago • 2 comments

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

Mantis: MT-1111
Submitted on: 2011-08-29 by (at)mulbrich
Updated: 2013-01-18
Assigned to: (at)mulbrich

Description

I tried to save the result of an interactive proof which I have been conducting for a couple of hours. Unfortunately, a strange error message popped up instead of saving the file.

Steps to reproduce

I do not know which steps were responsible for the error.

Additional Information

java.lang.ClassCastException: de.uka.ilkd.key.proof.mgt.ComplexRuleJustificationBySpec cannot be cast to de.uka.ilkd.key.proof.mgt.RuleJustificationBySpec
	at de.uka.ilkd.key.proof.ProofSaver.printSingleNode(ProofSaver.java:208)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:232)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.node2Proof(ProofSaver.java:268)
	at de.uka.ilkd.key.proof.ProofSaver.save(ProofSaver.java:117)
	at de.uka.ilkd.key.gui.MainWindow.saveProof(MainWindow.java:1052)
	at de.uka.ilkd.key.gui.actions.SaveFileAction.actionPerformed(SaveFileAction.java:38)
	at javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:2012)
	at javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2335)
	at javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:404)
	at javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:259)
	at javax.swing.AbstractButton.doClick(AbstractButton.java:374)
	at javax.swing.plaf.basic.BasicMenuItemUI.doClick(BasicMenuItemUI.java:829)
	at javax.swing.plaf.basic.BasicMenuItemUI$Handler.menuDragMouseReleased(BasicMenuItemUI.java:939)
	at javax.swing.JMenuItem.fireMenuDragMouseReleased(JMenuItem.java:585)
	at javax.swing.JMenuItem.processMenuDragMouseEvent(JMenuItem.java:482)
	at javax.swing.JMenuItem.processMouseEvent(JMenuItem.java:428)
	at javax.swing.MenuSelectionManager.processMouseEvent(MenuSelectionManager.java:320)
	at javax.swing.plaf.basic.BasicPopupMenuUI$MouseGrabber.eventDispatched(BasicPopupMenuUI.java:860)
	at java.awt.Toolkit$SelectiveAWTEventListener.eventDispatched(Toolkit.java:2378)
	at java.awt.Toolkit$ToolkitEventMulticaster.eventDispatched(Toolkit.java:2270)
	at java.awt.Toolkit.notifyAWTEventListeners(Toolkit.java:2228)
	at java.awt.Component.dispatchEventImpl(Component.java:4460)
	at java.awt.Container.dispatchEventImpl(Container.java:2163)
	at java.awt.Component.dispatchEvent(Component.java:4390)
	at java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4461)
	at java.awt.LightweightDispatcher.processMouseEvent(Container.java:4125)
	at java.awt.LightweightDispatcher.dispatchEvent(Container.java:4055)
	at java.awt.Container.dispatchEventImpl(Container.java:2149)
	at java.awt.Window.dispatchEventImpl(Window.java:2478)
	at java.awt.Component.dispatchEvent(Component.java:4390)
	at java.awt.EventQueue.dispatchEventImpl(EventQueue.java:649)
	at java.awt.EventQueue.access$000(EventQueue.java:96)
	at java.awt.EventQueue$1.run(EventQueue.java:608)
	at java.awt.EventQueue$1.run(EventQueue.java:606)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.security.AccessControlContext$1.doIntersectionPrivilege(AccessControlContext.java:105)
	at java.security.AccessControlContext$1.doIntersectionPrivilege(AccessControlContext.java:116)
	at java.awt.EventQueue$2.run(EventQueue.java:622)
	at java.awt.EventQueue$2.run(EventQueue.java:620)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.security.AccessControlContext$1.doIntersectionPrivilege(AccessControlContext.java:105)
	at java.awt.EventQueue.dispatchEvent(EventQueue.java:619)
	at java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:275)
	at java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:200)
	at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:190)
	at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:185)
	at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:177)
	at java.awt.EventDispatchThread.run(EventDispatchThread.java:138)
java.lang.ClassCastException: de.uka.ilkd.key.proof.mgt.ComplexRuleJustificationBySpec cannot be cast to de.uka.ilkd.key.proof.mgt.RuleJustificationBySpec
	at de.uka.ilkd.key.proof.ProofSaver.printSingleNode(ProofSaver.java:208)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:232)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.collectProof(ProofSaver.java:252)
	at de.uka.ilkd.key.proof.ProofSaver.node2Proof(ProofSaver.java:268)
	at de.uka.ilkd.key.proof.ProofSaver.save(ProofSaver.java:117)
	at de.uka.ilkd.key.gui.MainWindow.saveProof(MainWindow.java:1052)
	at de.uka.ilkd.key.gui.actions.SaveFileAction.actionPerformed(SaveFileAction.java:38)
	at javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:2012)
	at javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2335)
	at javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:404)
	at javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:259)
	at javax.swing.AbstractButton.doClick(AbstractButton.java:374)
	at javax.swing.plaf.basic.BasicMenuItemUI.doClick(BasicMenuItemUI.java:829)
	at javax.swing.plaf.basic.BasicMenuItemUI$Handler.menuDragMouseReleased(BasicMenuItemUI.java:939)
	at javax.swing.JMenuItem.fireMenuDragMouseReleased(JMenuItem.java:585)
	at javax.swing.JMenuItem.processMenuDragMouseEvent(JMenuItem.java:482)
	at javax.swing.JMenuItem.processMouseEvent(JMenuItem.java:428)
	at javax.swing.MenuSelectionManager.processMouseEvent(MenuSelectionManager.java:320)
	at javax.swing.plaf.basic.BasicPopupMenuUI$MouseGrabber.eventDispatched(BasicPopupMenuUI.java:860)
	at java.awt.Toolkit$SelectiveAWTEventListener.eventDispatched(Toolkit.java:2378)
	at java.awt.Toolkit$ToolkitEventMulticaster.eventDispatched(Toolkit.java:2270)
	at java.awt.Toolkit.notifyAWTEventListeners(Toolkit.java:2228)
	at java.awt.Component.dispatchEventImpl(Component.java:4460)
	at java.awt.Container.dispatchEventImpl(Container.java:2163)
	at java.awt.Component.dispatchEvent(Component.java:4390)
	at java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4461)
	at java.awt.LightweightDispatcher.processMouseEvent(Container.java:4125)
	at java.awt.LightweightDispatcher.dispatchEvent(Container.java:4055)
	at java.awt.Container.dispatchEventImpl(Container.java:2149)
	at java.awt.Window.dispatchEventImpl(Window.java:2478)
	at java.awt.Component.dispatchEvent(Component.java:4390)
	at java.awt.EventQueue.dispatchEventImpl(EventQueue.java:649)
	at java.awt.EventQueue.access$000(EventQueue.java:96)
	at java.awt.EventQueue$1.run(EventQueue.java:608)
	at java.awt.EventQueue$1.run(EventQueue.java:606)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.security.AccessControlContext$1.doIntersectionPrivilege(AccessControlContext.java:105)
	at java.security.AccessControlContext$1.doIntersectionPrivilege(AccessControlContext.java:116)
	at java.awt.EventQueue$2.run(EventQueue.java:622)
	at java.awt.EventQueue$2.run(EventQueue.java:620)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.security.AccessControlContext$1.doIntersectionPrivilege(AccessControlContext.java:105)
	at java.awt.EventQueue.dispatchEvent(EventQueue.java:619)
	at java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:275)
	at java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:200)
	at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:190)
	at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:185)
	at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:177)
	at java.awt.EventDispatchThread.run(EventDispatchThread.java:138)

Files

Notes

(at)scheben at 2012-01-25

I had the same error in a proof with 5487 nodes 60 branches 23 interactions

(at)rbubel at 2012-01-27

One question, did you in both cases work on a previous saved and reloaded proof? And/Or using Delayed Cut?

(at)scheben at 2012-01-27

No, at least in my case I did the proof from scratch and didn't use the delayed cut. However, most likely mattias has found the problem: it seems that the application of the UseDependenyContract rule jumps back under some circumstances without providing a justification for it's application. I think we will fix the bug during the next days.

(at)mulbrich at 2012-01-27

fixed in d82086d01ba7da9e98964b9d869b339eacccebba

History

(at)mulbrich -- (NEW_BUG) 2011-08-29
(at)grahl -- (BUG_MONITOR) 2011-12-06
(at)scheben -- (NORMAL_TYPE) 2012-01-25
(at)scheben -- (BUGNOTE_ADDED) 2012-01-25
(at)rbubel -- (BUGNOTE_ADDED) 2012-01-27
(at)rbubel -- (BUGNOTE_UPDATED) 2012-01-27
(at)scheben -- (BUGNOTE_ADDED) 2012-01-27
(at)mulbrich -- (BUGNOTE_ADDED) 2012-01-27
(at)mulbrich -- (NORMAL_TYPE) 2012-01-27
(at)mulbrich -- (NORMAL_TYPE) 2012-01-27
(at)mulbrich -- (NORMAL_TYPE) 2012-01-27
(at)mulbrich -- (NORMAL_TYPE) 2012-11-07
(at)grahl -- (NORMAL_TYPE) 2013-01-18
(at)grahl -- (NORMAL_TYPE) 2013-01-18

Attributes

Category: Proof Loading/Saving
Status: CLOSED
Severity: MAJOR
OS:
Target Version:
Resolution: FIXED
Priority: NORMAL
Reproducibility: HAVENOTTRIED
Platform:
Commit:
Build:
Tags []
Labels: ~Proof Loading/Saving ~Bug ~NORMAL

View in Mantis

Information:

created_at: 2017-05-29T02:48:20.498Z
updated_at: 2017-05-29T02:48:21.254Z
closed_at: 2017-05-29T02:48:21.215Z (closed_by: )
milestone:
user_notes_count: 0

Dec 23 '22 23:12 wadoon

key key copied to clipboard

Exception while saving proofs

Description

Steps to reproduce

Additional Information

Files

Notes

History

Attributes

key
key copied to clipboard