Skip to content

Commit d908b8f

Browse files
committed
fix ContractLoadingTest
1 parent 5057611 commit d908b8f

4 files changed

Lines changed: 3 additions & 28 deletions

File tree

key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java

Lines changed: 1 addition & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -387,7 +387,7 @@ private List<CompilationUnit> parseLibraryClasses(FileRepo fileRepo) throws IOEx
387387

388388
List<CompilationUnit> rcuList = new ArrayList<>();
389389

390-
// -- read files --
390+
// read files
391391
for (FileCollection fc : sources) {
392392
FileCollection.Walker walker = fc.createWalker(new String[] { ".jml", ".java" });
393393
while (walker.step()) {
@@ -404,27 +404,6 @@ private List<CompilationUnit> parseLibraryClasses(FileRepo fileRepo) throws IOEx
404404
}
405405
}
406406
}
407-
408-
// -- read class files --
409-
// TODO javaparser
410-
/*
411-
* ClassFileDeclarationManager manager = new ClassFileDeclarationManager(pf);
412-
* ByteCodeParser parser = new ByteCodeParser();
413-
* for (FileCollection fc : sources) {
414-
* FileCollection.Walker walker = fc.createWalker(".class");
415-
* while (walker.step()) {
416-
* currentDataLocation = walker.getCurrentDataLocation();
417-
* try (InputStream is = new BufferedInputStream(walker.openCurrent(fileRepo))) {
418-
* ClassFile cf = parser.parseClassFile(is);
419-
* manager.addClassFile(cf, currentDataLocation);
420-
* } catch (Exception ex) {
421-
* throw new ConvertException("Error while loading: " + walker.getCurrentDataLocation(),
422-
* ex);
423-
* }
424-
* }
425-
* }
426-
* rcuList.addAll(manager.getCompilationUnits());
427-
*/
428407
return rcuList;
429408
}
430409

key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLMethodResolver.java

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,6 @@ protected SLExpression doResolving(SLExpression receiver, String methodName,
4343
return null;
4444
}
4545

46-
// FIXME weigl this seems wrong. Should it not be that this
47-
// containingType=manager.specInClass?
4846
KeYJavaType containingType = receiver.getType();
4947
if (containingType == null) {
5048
return null;

key.core/src/test/resources/testcase/specMath/bigint/Test.java

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
// This test uses method resolution to return BigIntMarker or IntMarker from the accept model method
22
// Test failure is indicated by method resolution failing
3-
/*@ spec_bigint_math @*/
4-
public class Test {
3+
public /*@ spec_bigint_math @*/ class Test {
54
public static class BigIntMarker {
65
public boolean isBigint() {
76
return true;

key.core/src/test/resources/testcase/specMath/java/Test.java

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
// This test uses method resolution to return BigIntMarker or IntMarker from the accept model method
22
// Test failure is indicated by method resolution failing
3-
/*@ spec_java_math @*/
4-
public class Test {
3+
public /*@ spec_java_math @*/ class Test {
54
public static class BigIntMarker {
65
public boolean isBigint() {
76
return true;

0 commit comments

Comments
 (0)