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

Userdefined \sorts can't be used in .java files #3402

Open
FabianKof opened this issue Feb 12, 2024 · 0 comments
Open

Userdefined \sorts can't be used in .java files #3402

FabianKof opened this issue Feb 12, 2024 · 0 comments

Comments

@FabianKof
Copy link

Description

Please describe your concern in detail!

In JML you can't use userdefined \sorts from .key files

\javaSource ".";
\sorts{
  Tupel;
}
\chooseContract
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
@FabianKof FabianKof changed the title Benutzerdefinierte Datentypen nicht in .java verwendbar Userdefined \sorts can't be used in .java files Feb 12, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant