Bug when reloading a file with fixed type

[Robert-Brune]

Description

Reload of the project files still produce loading error,
even after the problem is fixed in the source file.

Workaround: Restart KeY

Reproducible

Always

Steps to reproduce

• Minimal Example:

public class Minimal {
  //this must be \map instead of \dl_map
  //@ ghost \dl_map test; 
}

• Load this class KeY, expected error is shown.
• Accessing this invalid file fails with error message.
• In external editor, change the broken line to:

//@ ghost \map test; 

• Different error is shown: Cannot invoke "de.uka.ilkd.key.java.declaration.TypeDeclaration.getPositionInfo()" because "td" is null, even though the specification is syntactically fine.

• Restarting KeY allows the opening of the (fixed) file without problem.

Stack trace:

Java Version set to openjdk 21
[00:41:43.843] INFO  Main - Memory: total 516.0 MB, max 8192.0 MB, free 502.00724029541016 MB
[00:41:43.965] INFO  Main - KeY Version 2.12.3 (internal: e586672632c3fbda05be6d30879f0abf58dabec4)
[00:41:43.965] INFO  Main - © Copyright 2001–2024 Karlsruhe Institute of Technology, Chalmers University of Technology, and Technische Universität Darmstadt
[00:41:43.966] INFO  Main - KeY is protected by the GNU General Public License
[00:41:43.966] INFO  Main - Using assertions
[00:41:44.214] INFO  KeyStrokeSettings - Use new configuration format at /Users/robert/.key/keystrokes.json
[00:41:44.217] INFO  KeyStrokeSettings - Save keyboard shortcuts to: /Users/robert/.key/keystrokes.properties
[00:41:44.226] INFO  KeyStrokeSettings - Save keyboard shortcuts to: /Users/robert/.key/keystrokes.json
[00:41:44.486] INFO  ColorSettings - Load color settings from file /Users/robert/.key/colors.json
[00:41:45.367] INFO  RunAllProofsAction - Use 'export KEY_RUNALLPROOFS_UI_FILE=<...>' to set the input file for RunAllProofsAction.
[00:41:45.479] INFO  ProofSettings - Load proof dependent settings from file /Users/robert/.key/proof-settings.json
[00:41:52.212] INFO  AbstractProblemLoader - Loading environment from /Users/robert/bugKeY
[00:41:52.278] INFO  AbstractProblemLoader - Creating init config
[00:41:54.953] ERROR WindowUserInterfaceControl - de.uka.ilkd.key.proof.init.ProofInputException: Error in file /Users/robert/bugKeY/Test.java: called method public de.uka.ilkd.key.java.reference.TypeReference de.uka.ilkd.key.java.Recoder2KeYConverter.convert(recoder.java.reference.TypeReference) threw exception.
        at de.uka.ilkd.key.proof.init.ProblemInitializer.readJava(ProblemInitializer.java:289)
        at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:535)
        at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:460)
        at de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:543)
        at de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:310)
        at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:274)
        at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:74)
        at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:124)
        at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:117)
        at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:305)
        at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
        at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:342)
        at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
        at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
        at java.base/java.lang.Thread.run(Thread.java:1583)
Caused by: de.uka.ilkd.key.java.ParseExceptionInFile: Error in file /Users/robert/bugKeY/Test.java: called method public de.uka.ilkd.key.java.reference.TypeReference de.uka.ilkd.key.java.Recoder2KeYConverter.convert(recoder.java.reference.TypeReference) threw exception.
        at de.uka.ilkd.key.java.Recoder2KeY.readCompilationUnitsAsFiles(Recoder2KeY.java:316)
        at de.uka.ilkd.key.proof.init.ProblemInitializer.readJava(ProblemInitializer.java:287)
        ... 14 common frames omitted
Caused by: de.uka.ilkd.key.java.ConvertException: called method public de.uka.ilkd.key.java.reference.TypeReference de.uka.ilkd.key.java.Recoder2KeYConverter.convert(recoder.java.reference.TypeReference) threw exception.
        at de.uka.ilkd.key.java.Recoder2KeY.reportErrorWithPositionInFile(Recoder2KeY.java:1291)
        at de.uka.ilkd.key.java.Recoder2KeY.reportError(Recoder2KeY.java:1280)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:286)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildren(Recoder2KeYConverter.java:318)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:1016)
        at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
        at java.base/java.lang.reflect.Method.invoke(Method.java:580)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:273)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildren(Recoder2KeYConverter.java:318)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:959)
        at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
        at java.base/java.lang.reflect.Method.invoke(Method.java:580)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:273)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildren(Recoder2KeYConverter.java:318)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildrenAndComments(Recoder2KeYConverter.java:373)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:1970)
        at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
        at java.base/java.lang.reflect.Method.invoke(Method.java:580)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:273)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.process(Recoder2KeYConverter.java:86)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.processCompilationUnit(Recoder2KeYConverter.java:98)
        at de.uka.ilkd.key.java.Recoder2KeY.readCompilationUnitsAsFiles(Recoder2KeY.java:314)
        ... 15 common frames omitted
Caused by: java.lang.IllegalStateException: Could not find sort map for type: \dl_map
        at de.uka.ilkd.key.java.JavaInfo.getPrimitiveKeYJavaType(JavaInfo.java:333)
        at de.uka.ilkd.key.java.JavaInfo.getKeYJavaType(JavaInfo.java:484)
        at de.uka.ilkd.key.java.TypeConverter.getPrimitiveSort(TypeConverter.java:491)
        at de.uka.ilkd.key.java.Recoder2KeYTypeConverter.getKeYJavaType(Recoder2KeYTypeConverter.java:161)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.getKeYJavaType(Recoder2KeYConverter.java:178)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:1344)
        at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
        at java.base/java.lang.reflect.Method.invoke(Method.java:580)
        at de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:273)
        ... 34 common frames omitted

[00:42:09.215] INFO  AbstractProblemLoader - Loading environment from /Users/robert/bugKeY
[00:42:09.215] INFO  AbstractProblemLoader - Creating init config
[00:42:09.861] ERROR WindowUserInterfaceControl - java.lang.NullPointerException: Cannot invoke "de.uka.ilkd.key.java.declaration.TypeDeclaration.getPositionInfo()" because "td" is null
        at de.uka.ilkd.key.speclang.jml.JMLSpecExtractor.extractMethodSpecs(JMLSpecExtractor.java:369)
        at de.uka.ilkd.key.speclang.SLEnvInput.createSpecs(SLEnvInput.java:331)
        at de.uka.ilkd.key.speclang.SLEnvInput.read(SLEnvInput.java:393)
        at de.uka.ilkd.key.proof.init.ProblemInitializer.readEnvInput(ProblemInitializer.java:336)
        at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:569)
        at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:460)
        at de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:543)
        at de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:310)
        at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:274)
        at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:74)
        at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:124)
        at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:117)
        at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:305)
        at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
        at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:342)
        at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
        at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
        at java.base/java.lang.Thread.run(Thread.java:1583)

---

• Commit: INFO Main - KeY Version 2.12.3 (internal: e586672)