FabianKof
commented
6 months ago
## Description
> Please describe your concern in detail!
In JML you can't use userdefined \sorts from .key files
```
\javaSource ".";
\sorts{
Tupel;
}
\chooseContract
```
```java
class A{
\\@ public ghost \dl_Tupel t;
}
```
## Reproducible
always
### Steps to reproduce
1. Create the .key and .java file mentoned above
2. Put both in the same directory
3. Load the .key file in KeY
> What is your expected behavior and what was the actual behavior?
### it should load, actual behaviour
Error in file C:\Users\naiba\Desktop\BA\KeY testing\eigener Typ\.\A.java: called method public de.uka.ilkd.key.java.reference.TypeReference de.uka.ilkd.key.java.Recoder2KeYConverter.convert(recoder.java.reference.TypeReference) threw exception. Caused by: de.uka.ilkd.key.java.ParseExceptionInFile: Error in file C:\Users\naiba\Desktop\BA\KeY testing\eigener Typ\.\A.java: called method public de.uka.ilkd.key.java.reference.TypeReference de.uka.ilkd.key.java.Recoder2KeYConverter.convert(recoder.java.reference.TypeReference) threw exception.
> Add more details here. In particular: if you have a stacktrace, put it here.
```
de.uka.ilkd.key.proof.init.ProofInputException: Error in file C:\Users\naiba\Desktop\BA\KeY testing\eigener Typ\.\A.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:288)
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:557)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:319)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:277)
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 C:\Users\naiba\Desktop\BA\KeY testing\eigener Typ\.\A.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:313)
at de.uka.ilkd.key.proof.init.ProblemInitializer.readJava(ProblemInitializer.java:286)
... 14 more
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:1289)
at de.uka.ilkd.key.java.Recoder2KeY.reportError(Recoder2KeY.java:1278)
at de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:284)
at de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildren(Recoder2KeYConverter.java:316)
at de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:1009)
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:271)
at de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildren(Recoder2KeYConverter.java:316)
at de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:952)
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:271)
at de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildren(Recoder2KeYConverter.java:316)
at de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildrenAndComments(Recoder2KeYConverter.java:371)
at de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:1946)
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:271)
at de.uka.ilkd.key.java.Recoder2KeYConverter.process(Recoder2KeYConverter.java:84)
at de.uka.ilkd.key.java.Recoder2KeYConverter.processCompilationUnit(Recoder2KeYConverter.java:96)
at de.uka.ilkd.key.java.Recoder2KeY.readCompilationUnitsAsFiles(Recoder2KeY.java:311)
... 15 more
Caused by: java.lang.IllegalStateException: Could not find sort Tupel for type: \dl_Tupel
at de.uka.ilkd.key.java.JavaInfo.getPrimitiveKeYJavaType(JavaInfo.java:334)
at de.uka.ilkd.key.java.JavaInfo.getKeYJavaType(JavaInfo.java:485)
at de.uka.ilkd.key.java.TypeConverter.getPrimitiveSort(TypeConverter.java:476)
at de.uka.ilkd.key.java.Recoder2KeYTypeConverter.getKeYJavaType(Recoder2KeYTypeConverter.java:160)
at de.uka.ilkd.key.java.Recoder2KeYConverter.getKeYJavaType(Recoder2KeYConverter.java:176)
at de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:1325)
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:271)
... 34 more
```
* Commit: df9dc75fcaf1b75d47869a680d9a2316cdae364e