TestJavaCardDLJavaExtensions

2

tests

0

failures

0

ignored

7.908s

duration

100%

successful

Tests

Test Duration Result
testMethodFrameRedirectsScope() 3.878s passed
testTypeNotInScopeShouldNotBeFound() 4.030s passed

Standard output

33260      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ldt.key 
33260      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ldt.key 
34573      DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\javacardDLExtensions\src\test\TestJavaCardDLExtensions.java 
34573      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\javacardDLExtensions\typeResolutionInMethodFrame.key 
34588      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
34588      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
37199      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from src\test\resources\testcase\javacardDLExtensions\typeResolutionInMethodFrame.key 
37199      DEBUG Test worker     d.u.i.k.j.Recoder2KeYConverter recoder2key: called method public de.uka.ilkd.key.java.reference.TypeReference de.uka.ilkd.key.java.Recoder2KeYConverter.convert(recoder.java.reference.TypeReference) threw exception  de.uka.ilkd.key.util.ExceptionHandlerException: Recoder: 1 errors have occurred - aborting.
	at de.uka.ilkd.key.util.KeYRecoderExcHandler.recoderExitAction(KeYRecoderExcHandler.java:69)
Caused by: recoder.service.UnresolvedReferenceException: Could not resolve TypeReference "TestJavaCardDLExtensions" @1/3 in INTERNAL:<virtual_class_for_parsing174>(14)
	at recoder.service.DefaultSourceInfo.getType(DefaultSourceInfo.java:798)

37199      DEBUG Test worker     d.u.i.k.j.Recoder2KeYConverter recoder2key: called method public de.uka.ilkd.key.java.declaration.LocalVariableDeclaration de.uka.ilkd.key.java.Recoder2KeYConverter.convert(recoder.java.declaration.LocalVariableDeclaration) threw exception  de.uka.ilkd.key.java.PosConvertException: 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:1254)
Caused by: recoder.service.UnresolvedReferenceException: Could not resolve TypeReference "TestJavaCardDLExtensions" @1/3 in INTERNAL:<virtual_class_for_parsing174>(14)
	at recoder.service.DefaultSourceInfo.getType(DefaultSourceInfo.java:798)

37199      DEBUG Test worker     d.u.i.k.j.Recoder2KeYConverter recoder2key: called method public de.uka.ilkd.key.java.StatementBlock de.uka.ilkd.key.java.Recoder2KeYConverter.convert(recoder.java.StatementBlock) threw exception  de.uka.ilkd.key.java.PosConvertException: 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:1254)
Caused by: recoder.service.UnresolvedReferenceException: Could not resolve TypeReference "TestJavaCardDLExtensions" @1/3 in INTERNAL:<virtual_class_for_parsing174>(14)
	at recoder.service.DefaultSourceInfo.getType(DefaultSourceInfo.java:798)

38575      DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\javacardDLExtensions\src\test\TestJavaCardDLExtensions.java 
38575      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\javacardDLExtensions\typeResolutionInMethodFrame2.key 
38590      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
38590      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
41077      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from src\test\resources\testcase\javacardDLExtensions\typeResolutionInMethodFrame2.key