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

Errors in rule files are lost and reported as malformed URLs #1529

Closed
wadoon opened this issue Dec 23, 2022 · 0 comments
Closed

Errors in rule files are lost and reported as malformed URLs #1529

wadoon opened this issue Dec 23, 2022 · 0 comments

Comments

@wadoon
Copy link
Member

wadoon commented Dec 23, 2022

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


Description

If there is a parsing error in one of the rule files in KeY,
KeY does not load, but does not report an error. Only in the status line
it reports

Failed to load JML specifications

This is a false error report.

Reproducible

Reproducible

Steps to reproduce

Go and touch one file in key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ such that it contains
a syntax error.

This error should be reported. But it is not.

Additional information

Debugging reveals that the URL string is

file://jar:file:/home/SOMEPATH/key/key/key.core/build/libs/key.core-2.7.jar!/de/uka/ilkd/key/proof/rules/javaRules.key

which is bound to fail

Exception in thread "AWT-EventQueue-0" java.lang.RuntimeException: java.net.MalformedURLException: For input string: "file:"
        at de.uka.ilkd.key.parser.Location.<init>(Location.java:63)
        at de.uka.ilkd.key.util.ExceptionTools.getLocation(ExceptionTools.java:51)
        at de.uka.ilkd.key.util.ExceptionTools.getLocation(ExceptionTools.java:98)
        at de.uka.ilkd.key.gui.ExceptionDialog.<init>(ExceptionDialog.java:62)
        at de.uka.ilkd.key.gui.ExceptionDialog.showDialog(ExceptionDialog.java:54)
        at de.uka.ilkd.key.gui.WindowUserInterfaceControl.taskFinished(WindowUserInterfaceControl.java:211)
        at de.uka.ilkd.key.proof.io.ProblemLoader.fireTaskFinished(ProblemLoader.java:100)
        at de.uka.ilkd.key.proof.io.ProblemLoader.access$200(ProblemLoader.java:38)
        at de.uka.ilkd.key.proof.io.ProblemLoader$1.done(ProblemLoader.java:139)
        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:313)
        at javax.swing.Timer$DoPostEvent.run(Timer.java:245)
        at java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:311)
        at java.awt.EventQueue.dispatchEventImpl(EventQueue.java:758)
        at java.awt.EventQueue.access$500(EventQueue.java:97)
        at java.awt.EventQueue$3.run(EventQueue.java:709)
        at java.awt.EventQueue$3.run(EventQueue.java:703)
        at java.security.AccessController.doPrivileged(Native Method)
        at java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:74)
        at java.awt.EventQueue.dispatchEvent(EventQueue.java:728)
        at java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:205)
        at java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:116)
        at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:105)
        at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
        at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:93)
        at java.awt.EventDispatchThread.run(EventDispatchThread.java:82)
Caused by: java.net.MalformedURLException: For input string: "file:"
        at java.net.URL.<init>(URL.java:627)
        at java.net.URL.<init>(URL.java:490)
        at java.net.URL.<init>(URL.java:439)
        at de.uka.ilkd.key.parser.Location.<init>(Location.java:61)
        ... 28 more
Caused by: java.lang.NumberFormatException: For input string: "file:"
        at java.lang.NumberFormatException.forInputString(NumberFormatException.java:65)
        at java.lang.Integer.parseInt(Integer.java:580)
        at java.lang.Integer.parseInt(Integer.java:615)
        at java.net.URLStreamHandler.parseURL(URLStreamHandler.java:222)
        at sun.net.www.protocol.file.Handler.parseURL(Handler.java:67)
        at java.net.URL.<init>(URL.java:622)
        ... 31 more

  • Commit: 585afa6b13e1642fe76998ed2465ff717c0b1f70
  • Component: ~"Proof Loading/Saving"

Information:

  • created_at: 2020-02-12T23:12:32.808Z
  • updated_at: 2021-07-27T10:12:51.178Z
  • closed_at: 2021-07-27T10:12:51.174Z (closed_by: pfeifer)
  • milestone:
  • user_notes_count: 1
@wadoon wadoon changed the title <placeholder> Errors in rule files are lost and reported as malformed URLs Dec 24, 2022
@wadoon wadoon closed this as completed Dec 24, 2022
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

1 participant