JavacExtension does not work with classpath/bootclasspath

[WolframPfeifer]

Description

When a .key/.proof file is loaded which contains a \bootclasspath directive, the Javac extensions crashes.

The bug was originally found by @unp1.

Reproducible

always

Steps to reproduce

1. Load the attached proof bundle bcptest.zip (just change the extension to "zproof").
2. Select the dummy proof, which makes use of the bootclasspath and classpath options.

The Javac extension hangs and never gets out of this state again:

The reason seems to be a wrong parameter that is passed to the Java compiler (-Xbootclasspath):

Exception in thread "AWT-EventQueue-0" java.lang.IllegalArgumentException: error: invalid flag: -Xbootclasspath
	at jdk.compiler/com.sun.tools.javac.main.Arguments.reportDiag(Arguments.java:886)
	at jdk.compiler/com.sun.tools.javac.main.Arguments.doProcessArgs(Arguments.java:396)
	at jdk.compiler/com.sun.tools.javac.main.Arguments.processArgs(Arguments.java:348)
	at jdk.compiler/com.sun.tools.javac.main.Arguments.init(Arguments.java:247)
	at jdk.compiler/com.sun.tools.javac.api.JavacTool.getTask(JavacTool.java:191)
	at jdk.compiler/com.sun.tools.javac.api.JavacTool.getTask(JavacTool.java:119)
	at jdk.compiler/com.sun.tools.javac.api.JavacTool.getTask(JavacTool.java:68)
	at de.uka.ilkd.key.gui.plugins.javac.JavaCompilerCheckFacade.check(JavaCompilerCheckFacade.java:114)
	at de.uka.ilkd.key.gui.plugins.javac.JavacExtension.loadProof(JavacExtension.java:157)
	at de.uka.ilkd.key.gui.plugins.javac.JavacExtension.selectedProofChanged(JavacExtension.java:228)
	at de.uka.ilkd.key.core.KeYSelectionModel.fireSelectedProofChanged(KeYSelectionModel.java:375)
	at de.uka.ilkd.key.core.KeYSelectionModel.setSelectedProof(KeYSelectionModel.java:84)
	at de.uka.ilkd.key.gui.MainWindow.lambda$addProblem$13(MainWindow.java:1190)

If the button is pressed in this state, an NPE is triggered:

Exception in thread "AWT-EventQueue-0" java.lang.NullPointerException: Cannot invoke "java.util.List.isEmpty()" because "data.issues" is null
	at de.uka.ilkd.key.gui.plugins.javac.JavacExtension.lambda$new$0(JavacExtension.java:111)
	at java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1972)
	at java.desktop/javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2314)
	at java.desktop/javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:407)
	at java.desktop/javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:262)
	at java.desktop/javax.swing.plaf.basic.BasicButtonListener.mouseReleased(BasicButtonListener.java:279)
        ...

Additional information

The issue seems easy to fix at first: When changing "-Xbootclasspath" to "-bootclasspath", at works without error. However, I am not sure if this is the desired behavior: Errors in bootclasspath/classpath can not be detected this way, since with these parameters Java only looks for already compiled classes, and just ignores the .java files (as far as I understand).

What I would expect is that also bootclasspath and classpath directories are checked for compilation errors. However, since we allow Java without method bodies in bootclasspath (and also in classpath, I guess), we can not just run javac on it. This would result in lots of errors. So maybe the only option for now is to ignore bootclasspath/classpath in the extension, and maybe give a warning (at least in the log) that these cannot be checked at the moment.