testLoadingOfTwoDifferentProofFiles()
An error occurred while parsing the libraries (file: src/test/resources/testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__a()]_JML_normal_behavior_operation_contract_0.proof; caused by: de.uka.ilkd.key.java.ConvertException: An error occurred while parsing the libraries)
at app//de.uka.ilkd.key.control.AbstractUserInterfaceControl.load(AbstractUserInterfaceControl.java:228)
at app//de.uka.ilkd.key.control.KeYEnvironment.load(KeYEnvironment.java:283)
at app//de.uka.ilkd.key.control.KeYEnvironment.load(KeYEnvironment.java:252)
at app//de.uka.ilkd.key.control.KeYEnvironment.load(KeYEnvironment.java:226)
at app//de.uka.ilkd.key.parser.TestParallelParsing$LoadThread.run(TestParallelParsing.java:113)
Caused by: de.uka.ilkd.key.java.ConvertException: An error occurred while parsing the libraries
at app//de.uka.ilkd.key.java.Recoder2KeY.reportErrorWithPositionInFile(Recoder2KeY.java:1246)
at app//de.uka.ilkd.key.java.Recoder2KeY.reportError(Recoder2KeY.java:1236)
at app//de.uka.ilkd.key.java.Recoder2KeY.parseSpecialClasses(Recoder2KeY.java:728)
at app//de.uka.ilkd.key.java.Recoder2KeY.recoderCompilationUnitsAsFiles(Recoder2KeY.java:356)
at app//de.uka.ilkd.key.java.Recoder2KeY.readCompilationUnitsAsFiles(Recoder2KeY.java:292)
at app//de.uka.ilkd.key.proof.init.ProblemInitializer.readJava(ProblemInitializer.java:282)
at app//de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:520)
at app//de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:455)
at app//de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:549)
at app//de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:312)
at app//de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:276)
at app//de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:258)
at app//de.uka.ilkd.key.control.AbstractUserInterfaceControl.load(AbstractUserInterfaceControl.java:215)
... 4 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 app//de.uka.ilkd.key.java.Recoder2KeY.reportErrorWithPositionInFile(Recoder2KeY.java:1246)
at app//de.uka.ilkd.key.java.Recoder2KeY.reportError(Recoder2KeY.java:1236)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:288)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildren(Recoder2KeYConverter.java:320)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:1010)
at jdk.internal.reflect.GeneratedMethodAccessor25.invoke(Unknown Source)
at java.base@11.0.18/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base@11.0.18/java.lang.reflect.Method.invoke(Method.java:566)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:275)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildren(Recoder2KeYConverter.java:320)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:953)
at jdk.internal.reflect.GeneratedMethodAccessor37.invoke(Unknown Source)
at java.base@11.0.18/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base@11.0.18/java.lang.reflect.Method.invoke(Method.java:566)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:275)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildren(Recoder2KeYConverter.java:320)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildrenAndComments(Recoder2KeYConverter.java:375)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:1946)
at jdk.internal.reflect.GeneratedMethodAccessor34.invoke(Unknown Source)
at java.base@11.0.18/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base@11.0.18/java.lang.reflect.Method.invoke(Method.java:566)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:275)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.process(Recoder2KeYConverter.java:89)
at app//de.uka.ilkd.key.java.Recoder2KeYConverter.processCompilationUnit(Recoder2KeYConverter.java:101)
at app//de.uka.ilkd.key.java.Recoder2KeY.parseLibraryClasses0(Recoder2KeY.java:773)
at app//de.uka.ilkd.key.java.Recoder2KeY.parseSpecialClasses(Recoder2KeY.java:726)
... 14 more
Caused by: java.lang.IllegalArgumentException: ProofJava produced column 0
at de.uka.ilkd.key.java.Position.fromPosition(Position.java:88)
at de.uka.ilkd.key.java.Recoder2KeYConverter.positionInfo(Recoder2KeYConverter.java:389)
at de.uka.ilkd.key.java.Recoder2KeYConverter.collectChildren(Recoder2KeYConverter.java:331)
at de.uka.ilkd.key.java.Recoder2KeYConverter.convert(Recoder2KeYConverter.java:1326)
at jdk.internal.reflect.GeneratedMethodAccessor6.invoke(Unknown Source)
at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base/java.lang.reflect.Method.invoke(Method.java:566)
at de.uka.ilkd.key.java.Recoder2KeYConverter.callConvert(Recoder2KeYConverter.java:275)
... 37 more