Skip to content

Exceptions in fresh KeY installation [macOS] (3.0) #3908

Description

@Robert-Brune

Description

After removing the .key directory from a previous installation KeY is not able to start anymore.

Reproducible

Fully reproducible.
Tested on macOS.

Steps to reproduce

A:

  1. cd ~
  2. mv .key .key-old
  3. java -jar key-3.0.0-dev-exe.jar

KeY is not able to start and produces the following exceptions (see logs).
No UI available.

B:

  1. cd ~
  2. mv .key .key-old
  3. Create old default folders: java -jar key-2.12.3-exe.jar
  4. java -jar key-3.0.0-dev-exe.jar

KeY is able to start but still produces the following exception (see logs).
UI becomes available.

Additional information

A:

[15:14:22.126] INFO  Main - The configuration folder is here /Users/robert/.key/v3.0
[15:14:22.128] INFO  Main - Assertion evaluation is disabled.
[15:14:22.129] INFO  Main - Memory: total 516.0 MB, max 8192.0 MB, free 480.0877990722656 MB
[15:14:22.232] INFO  Main - KeY Version 3.0.0-dev (internal: b99d9b615b6a3eeb276c924226e62365a4eeda9e)
[15:14:22.232] INFO  Main - © Copyright 2001–2024 Karlsruhe Institute of Technology, Chalmers University of Technology, and Technische Universität Darmstadt
[15:14:22.232] INFO  Main - KeY is protected by the GNU General Public License
[15:14:22.232] INFO  Main - Debug.ENABLE_ASSERTION = true
java.lang.RuntimeException: java.lang.reflect.InvocationTargetException
	at de.uka.ilkd.key.gui.MainWindow.getInstance(MainWindow.java:430)
	at de.uka.ilkd.key.gui.MainWindow.getInstance(MainWindow.java:411)
	at de.uka.ilkd.key.core.Main.createUserInterface(Main.java:434)
	at de.uka.ilkd.key.core.Main.call(Main.java:345)
	at de.uka.ilkd.key.core.Main.call(Main.java:56)
	at picocli.CommandLine.executeUserObject(CommandLine.java:2031)
	at picocli.CommandLine.access$1500(CommandLine.java:148)
	at picocli.CommandLine$RunLast.executeUserObjectOfLastSubcommandWithSameParent(CommandLine.java:2469)
	at picocli.CommandLine$RunLast.handle(CommandLine.java:2461)
	at picocli.CommandLine$RunLast.handle(CommandLine.java:2423)
	at picocli.CommandLine$AbstractParseResultHandler.execute(CommandLine.java:2277)
	at picocli.CommandLine$RunLast.execute(CommandLine.java:2425)
	at picocli.CommandLine.execute(CommandLine.java:2174)
	at de.uka.ilkd.key.core.Main.main(Main.java:228)
Caused by: java.lang.reflect.InvocationTargetException
	at java.desktop/java.awt.EventQueue.invokeAndWait(EventQueue.java:1371)
	at java.desktop/java.awt.EventQueue.invokeAndWait(EventQueue.java:1346)
	at java.desktop/javax.swing.SwingUtilities.invokeAndWait(SwingUtilities.java:1480)
	at de.uka.ilkd.key.gui.MainWindow.getInstance(MainWindow.java:428)
	... 13 more
Caused by: java.lang.NullPointerException: Cannot invoke "de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeSettings.getKeyStroke(String, javax.swing.KeyStroke)" because the return value of "de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeSettings.getInstance()" is null
	at de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.get(KeyStrokeManager.java:69)
	at de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.get(KeyStrokeManager.java:93)
	at de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.get(KeyStrokeManager.java:104)
	at de.uka.ilkd.key.gui.actions.MainWindowAction.<init>(MainWindowAction.java:36)
	at de.uka.ilkd.key.gui.actions.HidePackagePrefixToggleAction.<init>(HidePackagePrefixToggleAction.java:33)
	at de.uka.ilkd.key.gui.MainWindow.<init>(MainWindow.java:166)
	at de.uka.ilkd.key.gui.MainWindow.getInstance(MainWindow.java:437)
	at de.uka.ilkd.key.gui.MainWindow.getInstance(MainWindow.java:411)
	at java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:308)
	at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:773)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:720)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:714)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:400)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:87)
	at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:742)
	at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
	at java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)

B:

[15:14:38.533] INFO  Main - The configuration folder is here /Users/robert/.key/v3.0
[15:14:38.534] INFO  Main - Assertion evaluation is disabled.
[15:14:38.535] INFO  Main - Memory: total 516.0 MB, max 8192.0 MB, free 480.54344940185547 MB
[15:14:38.636] INFO  Main - KeY Version 3.0.0-dev (internal: b99d9b615b6a3eeb276c924226e62365a4eeda9e)
[15:14:38.636] INFO  Main - © Copyright 2001–2024 Karlsruhe Institute of Technology, Chalmers University of Technology, and Technische Universität Darmstadt
[15:14:38.636] INFO  Main - KeY is protected by the GNU General Public License
[15:14:38.636] INFO  Main - Debug.ENABLE_ASSERTION = true
[15:14:38.881] INFO  KeyStrokeSettings - Use new configuration format at /Users/robert/.key/v3.0/keystrokes.json
[15:14:38.884] INFO  KeyStrokeSettings - Save keyboard shortcuts to: /Users/robert/.key/v3.0/keystrokes.json
[15:14:38.884] INFO  KeyStrokeSettings - Save keyboard shortcuts to: /Users/robert/.key/v3.0/keystrokes.json
[15:14:39.135] INFO  ColorSettings - Load color settings from file /Users/robert/.key/v3.0/colors.json
[15:14:39.960] INFO  RunAllProofsAction - Use 'export KEY_RUNALLPROOFS_UI_FILE=<...>' to set the input file for RunAllProofsAction.
[15:14:40.044] WARN  ProofSettings - No proof-settings could be loaded, using defaultsjava.nio.file.NoSuchFileException: /Users/robert/.key/v3.0/proof-settings.json
	at java.base/sun.nio.fs.UnixException.translateToIOException(UnixException.java:92)
	at java.base/sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:106)
	at java.base/sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:111)
	at java.base/sun.nio.fs.UnixFileSystemProvider.newByteChannel(UnixFileSystemProvider.java:261)
	at java.base/java.nio.file.Files.newByteChannel(Files.java:380)
	at java.base/java.nio.file.Files.newByteChannel(Files.java:432)
	at java.base/java.nio.file.spi.FileSystemProvider.newInputStream(FileSystemProvider.java:420)
	at java.base/java.nio.file.Files.newInputStream(Files.java:160)
	at java.base/java.nio.file.Files.newBufferedReader(Files.java:2910)
	at de.uka.ilkd.key.settings.ProofSettings.loadSettings(ProofSettings.java:223)
	at de.uka.ilkd.key.settings.ProofSettings.loadedSettings(ProofSettings.java:63)
	at de.uka.ilkd.key.settings.ProofSettings.<clinit>(ProofSettings.java:58)
	at de.uka.ilkd.key.gui.settings.TacletOptionsSettings.<init>(TacletOptionsSettings.java:59)
	at de.uka.ilkd.key.gui.settings.SettingsManager.<clinit>(SettingsManager.java:38)
	at de.uka.ilkd.key.gui.MainWindow.createOptionsMenu(MainWindow.java:1139)
	at de.uka.ilkd.key.gui.MainWindow.createMenuBar(MainWindow.java:973)
	at de.uka.ilkd.key.gui.MainWindow.layoutMain(MainWindow.java:593)
	at de.uka.ilkd.key.gui.MainWindow.<init>(MainWindow.java:353)
	at de.uka.ilkd.key.gui.MainWindow.getInstance(MainWindow.java:437)
	at de.uka.ilkd.key.gui.MainWindow.getInstance(MainWindow.java:411)
	at java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:308)
	at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:773)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:720)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:714)
	at java.base/java.security.AccessController.doPrivileged(AccessController.java:400)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:87)
	at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:742)
	at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
	at java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)

[15:14:40.278] INFO  IsabelleTranslationSettings - No settings present, resorting to default Isabelle settings
[15:14:40.279] INFO  IsabelleTranslationSettings - Created Isabelle session files at: /Users/robert/.key/v3.0/IsabelleTranslations
[15:14:43.204] INFO  KeyStrokeSettings - Save keyboard shortcuts to: /Users/robert/.key/v3.0/keystrokes.json
[15:14:43.204] INFO  ColorSettings - Save color settings to: /Users/robert/.key/v3.0/colors.json
[15:14:43.204] INFO  IsabelleTranslationSettings - Save Isabelle settings to: /Users/robert/.key/v3.0/isabelleSettings.json
[15:14:43.204] INFO  KeyStrokeSettings - Save keyboard shortcuts to: /Users/robert/.key/v3.0/keystrokes.json

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions