diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJPMapping.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJPMapping.java index 1331cc2a37d..e2597d53437 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJPMapping.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJPMapping.java @@ -1,19 +1,18 @@ package de.uka.ilkd.key.java; -import java.util.*; -import javax.annotation.Nonnull; -import javax.annotation.Nullable; - -import de.uka.ilkd.key.java.ast.ProgramElement; -import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; -import de.uka.ilkd.key.util.Debug; - import com.github.javaparser.ast.Node; import com.github.javaparser.resolution.declarations.ResolvedDeclaration; import com.github.javaparser.resolution.types.ResolvedType; +import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.util.Debug; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import javax.annotation.Nonnull; +import javax.annotation.Nullable; +import java.util.*; + /** * @author Alexander Weigl * @version 1 (05.03.22) @@ -88,8 +87,9 @@ public KeYJPMapping() { * * @param pe a recoder.ModelElement */ - public Optional resolvedTypeToKeY(ResolvedType pe) { - return Optional.ofNullable(typeMap.get(pe)); + @Nullable + public KeYJavaType resolvedTypeToKeY(ResolvedType pe) { + return typeMap.get(pe); } public ResolvedType resolveType(KeYJavaType pe) { @@ -98,12 +98,15 @@ public ResolvedType resolveType(KeYJavaType pe) { return res; } - public Optional nodeToKeY(Node rm) { - return Optional.ofNullable(map.get(rm)); + @Nullable + public ProgramElement nodeToKeY(Node rm) { + return map.get(rm); } - public Optional resolvedDeclarationToKeY(ResolvedDeclaration rm) { - return rm.toAst().flatMap(this::nodeToKeY); + @Nullable + public ProgramElement resolvedDeclarationToKeY(ResolvedDeclaration rm) { + var ast = rm.toAst(); + return ast.map(this::nodeToKeY).orElse(null); } @Nullable @@ -116,7 +119,7 @@ public void put(Node node, ProgramElement value) { var formerNode = revMap.putIfAbsent(value, node); if (formerValue != null && formerValue != value) LOGGER.error("Duplicate registration of value: {}, formerValue: {}", value, - formerValue); + formerValue); if (formerNode != null && formerNode != node) LOGGER.error("Duplicate registration of node: {}, formerNode: {}", node, formerNode); } @@ -128,7 +131,7 @@ public void put(ResolvedType rec, KeYJavaType key) { var formerType = typeMapRev.putIfAbsent(key, rec); if (formerType != null && !Objects.equals(rec, formerType)) LOGGER.error("Duplicate registration of resolved type: {}, former: {}", rec, - formerType); + formerType); } public boolean mapped(Node rec) { @@ -201,7 +204,7 @@ public int size() { * not * * @param b boolean indicating if the special classes have been - * parsed in + * parsed in */ public void parsedSpecial(boolean b) { parsedSpecial = b; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java index fe739f8f91d..cc1a9ea62ab 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java @@ -1,25 +1,5 @@ package de.uka.ilkd.key.java; -import java.util.*; -import java.util.stream.Collectors; -import java.util.stream.Stream; -import java.util.stream.StreamSupport; -import javax.annotation.Nonnull; -import javax.annotation.Nullable; - -import de.uka.ilkd.key.java.ast.ResolvedLogicalType; -import de.uka.ilkd.key.java.ast.abstraction.ArrayType; -import de.uka.ilkd.key.java.ast.abstraction.Field; -import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; -import de.uka.ilkd.key.java.ast.abstraction.Type; -import de.uka.ilkd.key.java.ast.declaration.*; -import de.uka.ilkd.key.java.loader.JP2KeYTypeConverter; -import de.uka.ilkd.key.logic.op.IProgramMethod; -import de.uka.ilkd.key.logic.op.ProgramMethod; - -import org.key_project.util.collection.ImmutableArray; -import org.key_project.util.collection.ImmutableList; - import com.github.javaparser.ast.AccessSpecifier; import com.github.javaparser.ast.CompilationUnit; import com.github.javaparser.ast.Modifier; @@ -35,9 +15,27 @@ import com.github.javaparser.resolution.types.ResolvedType; import com.github.javaparser.symbolsolver.javaparsermodel.declarations.DefaultConstructorDeclaration; import com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserMethodDeclaration; +import de.uka.ilkd.key.java.ast.ResolvedLogicalType; +import de.uka.ilkd.key.java.ast.abstraction.ArrayType; +import de.uka.ilkd.key.java.ast.abstraction.Field; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.Type; +import de.uka.ilkd.key.java.ast.declaration.*; +import de.uka.ilkd.key.java.loader.JP2KeYTypeConverter; +import de.uka.ilkd.key.logic.op.IProgramMethod; +import de.uka.ilkd.key.logic.op.ProgramMethod; +import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableList; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import javax.annotation.Nonnull; +import javax.annotation.Nullable; +import java.util.*; +import java.util.stream.Collectors; +import java.util.stream.Stream; +import java.util.stream.StreamSupport; + public class KeYProgModelInfo { @@ -99,8 +97,8 @@ public List getAllProgramMethods(KeYJavaType kjt) { List result = new ArrayList<>(methods.size()); for (var rm : methods) { var declaration = rec2key().resolvedDeclarationToKeY(rm); - if (declaration.isPresent()) { - result.add((IProgramMethod) declaration.get()); + if (declaration != null) { + result.add((IProgramMethod) declaration); } } return result; @@ -165,7 +163,7 @@ public boolean isFinal(KeYJavaType kjt) { * Checks whether subType is a subtype of superType or not. * * @return true if subType is subtype of superType, - * false in the other case. + * false in the other case. */ public boolean isSubtype(KeYJavaType subType, KeYJavaType superType) { return isSubtype(rec2key().resolveType(subType), rec2key().resolveType(superType)); @@ -173,7 +171,7 @@ public boolean isSubtype(KeYJavaType subType, KeYJavaType superType) { private boolean isSubtype(ResolvedType subType, ResolvedType superType) { return superType.isAssignableBy(subType); // TODO weigl check if it is the right method and - // order. + // order. } public boolean isPackage(String name) { @@ -213,8 +211,8 @@ public List getAllProgramMethodsLocallyDeclared(KeYJavaType ct) { for (MethodUsage methodUsage : rml) { if (methodUsage.getDeclaration() instanceof JavaParserMethodDeclaration) { var element = mapping.resolvedDeclarationToKeY(methodUsage.getDeclaration()); - if (element.isPresent()) { - result.add((ProgramMethod) element.get()); + if (element != null) { + result.add((ProgramMethod) element); } } } @@ -240,8 +238,8 @@ public List getConstructors(KeYJavaType ct) { continue; } var m = mapping.resolvedDeclarationToKeY(decl); - if (m.isPresent()) { - result.add((IProgramMethod) m.get()); + if (m != null) { + result.add((IProgramMethod) m); } } return result; @@ -251,13 +249,40 @@ public List getConstructors(KeYJavaType ct) { * retrieves the most specific constructor declared in the given type with * respect to the given signature * - * @param ct the KeYJavyType where to look for the constructor + * @param ct the KeYJavyType where to look for the constructor * @param signature IList representing the signature of the constructor * @return the most specific constructor declared in the given type */ + @Nullable public IProgramMethod getConstructor(KeYJavaType ct, ImmutableList signature) { - // TODO javaparser - throw new UnsupportedOperationException(); + var rt = getJavaParserType(ct).asReferenceType().getTypeDeclaration(); + if (rt.isPresent()) { + List sig = signature.stream().map(this::getJavaParserType).toList(); + + List constructors = rt.get().getConstructors(); + constr: for (var constructor : constructors) { + if (sig.size() != constructor.getNumberOfParams()) { + continue; + } + + if (sig.size() == 0) { // fast track for default constructor calls! + var ast = constructor.toAst().get(); + return (IProgramMethod) mapping.nodeToKeY(ast); + } + + // compare types of the parameters + List types = constructor.formalParameterTypes(); + for (int i = 0; i < types.size(); i++) { + if (!types.get(i).equals(sig.get(i))) { + break constr; + } + } + var ast = constructor.toAst().get(); + return (IProgramMethod) mapping.nodeToKeY(ast); + } + //((ClassOrInterfaceDeclaration) rt.get().toAst().get()).getConstructorByParameterTypes() + } + return null; } /** @@ -289,16 +314,16 @@ private IProgramMethod getImplicitMethod(KeYJavaType ct, String name) { * in the given type or in a supertype where it is visible for the * given type, and has a signature that is compatible to the given one. * - * @param ct the class type to get methods from. - * @param name the name of the methods in question. + * @param ct the class type to get methods from. + * @param name the name of the methods in question. * @param signature the statical type signature of a callee. * @return the IProgramMethods, if one is found, - * null if none or more than one IProgramMethod is found (in this case - * a debug output is written to console). + * null if none or more than one IProgramMethod is found (in this case + * a debug output is written to console). */ @Nullable public IProgramMethod getProgramMethod(@Nonnull KeYJavaType ct, String name, - Iterable signature) { + Iterable signature) { if (ct.getJavaType() instanceof ArrayType) { return getImplicitMethod(ct, name); } @@ -312,7 +337,7 @@ public IProgramMethod getProgramMethod(@Nonnull KeYJavaType ct, String name, .map(this::getJavaParserType).toList(); var method = MethodResolutionLogic.solveMethodInType(rct, name, jpSignature); return method.getDeclaration() - .map(d -> (IProgramMethod) mapping.resolvedDeclarationToKeY(d).orElseThrow()) + .map(d -> (IProgramMethod) Objects.requireNonNull(mapping.resolvedDeclarationToKeY(d))) .orElse(null); } @@ -321,12 +346,12 @@ public IProgramMethod getProgramMethod(@Nonnull KeYJavaType ct, String name, * in the given type or in a supertype where it is visible for the * given type, and has a signature that is compatible to the given one. * - * @param ct the class type to get methods from. - * @param name the name of the methods in question. + * @param ct the class type to get methods from. + * @param name the name of the methods in question. * @param signature the statical type signature of a callee. * @return the IProgramMethods, if one is found, - * null if none or more than one IProgramMethod is found (in this case - * a debug output is written to console). + * null if none or more than one IProgramMethod is found (in this case + * a debug output is written to console). */ public IProgramMethod getProgramMethod( @Nonnull KeYJavaType ct, String name, @@ -337,8 +362,8 @@ public IProgramMethod getProgramMethod( private List asKeYFieldsR(Stream rfl) { return rfl.flatMap( - it -> ((FieldDeclaration) mapping.resolvedDeclarationToKeY(it).orElseThrow()) - .getFieldSpecifications().stream()) + it -> ((FieldDeclaration) Objects.requireNonNull(mapping.resolvedDeclarationToKeY(it))) + .getFieldSpecifications().stream()) .collect(Collectors.toList()); } @@ -389,12 +414,12 @@ public List getAllVisibleFields(KeYJavaType ct) { */ private List getVisibleArrayFields(KeYJavaType arrayType) { final ImmutableArray members = - ((ArrayDeclaration) arrayType.getJavaType()).getMembers(); + ((ArrayDeclaration) arrayType.getJavaType()).getMembers(); List result = new ArrayList<>(); for (MemberDeclaration member : members) { if (member instanceof FieldDeclaration) { final ImmutableArray specs = - ((FieldDeclaration) member).getFieldSpecifications(); + ((FieldDeclaration) member).getFieldSpecifications(); for (FieldSpecification spec : specs) { result.add(spec); } @@ -408,7 +433,7 @@ private List getVisibleArrayFields(KeYJavaType arrayType) { .getDeclaredFields() .stream() .filter(f -> f.accessSpecifier() != AccessSpecifier.PRIVATE) - .map(f -> (Field) mapping.resolvedDeclarationToKeY(f).orElseThrow()) + .map(f -> (Field) Objects.requireNonNull(mapping.resolvedDeclarationToKeY(f))) .toList(); result.addAll(objectFields); return result; @@ -461,12 +486,12 @@ private List getAllDeclaredSupertypes(KeYJavaType ct) { * * @param rctl the ASTList to be converted * @return list of KeYJavaTypes representing the given recoder types in - * the same order + * the same order */ private List asKeYJavaTypes( final Stream rctl) { return rctl - .map(it -> rec2key().resolvedTypeToKeY(new ReferenceTypeImpl(it)).orElseThrow()) + .map(it -> Objects.requireNonNull(rec2key().resolvedTypeToKeY(new ReferenceTypeImpl(it)))) .collect(Collectors.toList()); } @@ -497,7 +522,7 @@ public List getAllSubtypes(KeYJavaType ct) { } public ImmutableList findImplementations(KeYJavaType ct, String name, - ImmutableList signature) { + ImmutableList signature) { var type = rec2key().resolveType(ct); if (!type.isReferenceType()) { return ImmutableList.of(); @@ -541,7 +566,7 @@ public ImmutableList findImplementations(KeYJavaType ct, String nam private ImmutableList recFindImplementations(TypeDeclaration ct, - String name, List signature, ImmutableList result) { + String name, List signature, ImmutableList result) { // TODO weigl does not compile, no idea what this should be // if (declaresApplicableMethods(ct, name, signature)) { // KeYJavaType r = (KeYJavaType) mapping.toKeY(ct); @@ -568,15 +593,15 @@ private ImmutableList recFindImplementations(TypeDeclaration ct, private boolean declaresApplicableMethods(MethodResolutionCapability ct, String name, - List signature) { + List signature) { var method = ct.solveMethod(name, signature, false); return method.isSolved(); } private boolean isDeclaringInterface(/* - * recoder.abstraction.ClassType ct, String name, - * List signature - */) { + * recoder.abstraction.ClassType ct, String name, + * List signature + */) { // TODO Weigl does not compile // Debug.assertTrue(ct.isInterface()); // List list = si.getMethods(ct); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java index daca2a8d1e2..ae839132659 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java @@ -633,14 +633,14 @@ public Object visit(FieldAccessExpr n, Void arg) { } var ast = target.toAst().orElseThrow(); - var other = (VariableDeclaration) mapping.nodeToKeY(ast) - .orElseGet(() -> accept(ast)); + var tmp = (VariableDeclaration) mapping.nodeToKeY(ast); + VariableDeclaration other = tmp == null ? accept(ast) : tmp; ProgramVariable pv = null; if (target instanceof JavaParserFieldDeclaration) { // Field declarations can have multiple variables var decl = ((JavaParserFieldDeclaration) target).getVariableDeclarator(); - var keyDecl = (VariableSpecification) mapping.nodeToKeY(decl).orElseThrow(); + var keyDecl = (VariableSpecification) mapping.nodeToKeY(decl); pv = (ProgramVariable) keyDecl.getProgramVariable(); } else { for (VariableSpecification variable : other.getVariables()) { @@ -691,8 +691,8 @@ private ClassOrInterfaceDeclaration getContainingClass(Node node) { @Override public Object visit(FieldDeclaration n, Void arg) { var existing = mapping.nodeToKeY(n); - if (existing.isPresent()) { - return existing.get(); + if (existing != null) { + return existing; } var pi = createPositionInfo(n); var c = createComments(n); @@ -886,14 +886,14 @@ public Object visit(NameExpr n, Void arg) { var ast = target.toAst().get(); // Make sure the field is already converted - var other = (VariableDeclaration) mapping.nodeToKeY(ast) - .orElseGet(() -> accept(ast)); + var tmp = (VariableDeclaration) mapping.nodeToKeY(ast); + VariableDeclaration other = tmp == null ? accept(ast) : tmp; var pi = createPositionInfo(n); var c = createComments(n); if (target instanceof JavaParserFieldDeclaration) { // Field declarations can have multiple variables var decl = ((JavaParserFieldDeclaration) target).getVariableDeclarator(); - var keyDecl = (VariableSpecification) mapping.nodeToKeY(decl).orElseThrow(); + var keyDecl = (VariableSpecification) Objects.requireNonNull(mapping.nodeToKeY(decl)); var pv = (ProgramVariable) keyDecl.getProgramVariable(); if (pv.isMember()) { // TODO javaparser prefix null? should we add default this? @@ -905,7 +905,7 @@ public Object visit(NameExpr n, Void arg) { if (target instanceof JavaParserVariableDeclaration) { // Variable declarations can have multiple variables var decl = ((JavaParserVariableDeclaration) target).getVariableDeclarator(); - var keyDecl = (VariableSpecification) mapping.nodeToKeY(decl).orElseThrow(); + var keyDecl = (VariableSpecification) Objects.requireNonNull(mapping.nodeToKeY(decl)); return (ProgramVariable) keyDecl.getProgramVariable(); } if (other.getVariables().size() == 1) { @@ -1209,8 +1209,8 @@ public Object visit(UnknownType n, Void arg) { @Override public Object visit(VariableDeclarationExpr n, Void arg) { var existing = mapping.nodeToKeY(n); - if (existing.isPresent()) { - return existing.get(); + if (existing != null) { + return existing; } TypeReference type = requireTypeReference(n.getVariable(0).getType()); var varsList = new ArrayList(n.getVariables().size()); @@ -1317,7 +1317,7 @@ private ProgramVariable getProgramVariableForFieldSpecification(FullVariableDecl } var spec = decl.decl; var varSpec = mapping.nodeToKeY(spec); - if (varSpec.isEmpty()) { + if (varSpec == null) { var t = spec.getType().resolve(); var classNode = findContainingClass(spec).orElseThrow(); var classType = new ReferenceTypeImpl(classNode.resolve()); @@ -1337,7 +1337,7 @@ private ProgramVariable getProgramVariableForFieldSpecification(FullVariableDecl compileTimeConstant); } } else { - pv = (ProgramVariable) ((VariableSpecification) varSpec.get()).getProgramVariable(); + pv = (ProgramVariable) ((VariableSpecification) varSpec).getProgramVariable(); } fieldSpecificationMapping.put(decl, pv); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYTypeConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYTypeConverter.java index 7efd967992e..2939cd94aeb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYTypeConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYTypeConverter.java @@ -1,8 +1,16 @@ package de.uka.ilkd.key.java.loader; -import javax.annotation.Nonnull; - -import de.uka.ilkd.key.java.*; +import com.github.javaparser.resolution.TypeSolver; +import com.github.javaparser.resolution.declarations.ResolvedReferenceTypeDeclaration; +import com.github.javaparser.resolution.declarations.ResolvedTypeDeclaration; +import com.github.javaparser.resolution.model.typesystem.ReferenceTypeImpl; +import com.github.javaparser.resolution.types.ResolvedArrayType; +import com.github.javaparser.resolution.types.ResolvedPrimitiveType; +import com.github.javaparser.resolution.types.ResolvedReferenceType; +import com.github.javaparser.resolution.types.ResolvedType; +import de.uka.ilkd.key.java.KeYJPMapping; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.TypeConverter; import de.uka.ilkd.key.java.ast.Expression; import de.uka.ilkd.key.java.ast.ResolvedLogicalType; import de.uka.ilkd.key.java.ast.abstraction.*; @@ -24,18 +32,14 @@ import de.uka.ilkd.key.logic.sort.Sort; import de.uka.ilkd.key.logic.sort.SortImpl; import de.uka.ilkd.key.util.AssertionFailure; - import org.key_project.util.ExtList; import org.key_project.util.collection.*; - -import com.github.javaparser.resolution.TypeSolver; -import com.github.javaparser.resolution.declarations.ResolvedReferenceTypeDeclaration; -import com.github.javaparser.resolution.declarations.ResolvedTypeDeclaration; -import com.github.javaparser.resolution.model.typesystem.ReferenceTypeImpl; -import com.github.javaparser.resolution.types.*; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import javax.annotation.Nonnull; +import java.util.Objects; + /** * provide means to convert recoder types to the corresponding KeY type structures. *

@@ -125,8 +129,8 @@ public KeYJavaType getKeYJavaType(ResolvedType type) { { // lookup in the cache var kjt = jp2KeY.resolvedTypeToKeY(type); - if (kjt.isPresent()) { - return kjt.get(); + if (kjt != null) { + return kjt; } } @@ -150,7 +154,7 @@ public KeYJavaType getKeYJavaType(ResolvedType type) { // usually this equals what was just added in the methods above // sometimes however, there is a 'legacy' type in the mapping, // which has priority - return jp2KeY.resolvedTypeToKeY(type).orElseThrow(); + return Objects.requireNonNull(jp2KeY.resolvedTypeToKeY(type)); } private void addPrimitiveType(ResolvedType type) { @@ -188,7 +192,7 @@ private void addArrayType(ResolvedArrayType type) { // I may not use JavaInfo here because the classes may not yet be cached! Type elemType = kjt.getJavaType(); var arraySort = ArraySort.getArraySort(kjt.getSort(), elemType, getObjectType().getSort(), - getCloneableType().getSort(), getSerializableType().getSort()); + getCloneableType().getSort(), getSerializableType().getSort()); var result = new KeYJavaType(arraySort); if (getSortsNamespace().lookup(arraySort.name()) == null) { getSortsNamespace().add(arraySort); @@ -197,7 +201,7 @@ private void addArrayType(ResolvedArrayType type) { storeInCache(type, result); // delayed creation of virtual array declarations to avoid cycles - var arrayKJT = jp2KeY.resolvedTypeToKeY(type).orElseThrow(); + var arrayKJT = Objects.requireNonNull(jp2KeY.resolvedTypeToKeY(type)); var arrayType = createArrayType(getKeYJavaType(componentType), arrayKJT); result.setJavaType(arrayType); } @@ -273,7 +277,7 @@ private ImmutableSet directSuperSorts(ResolvedReferenceTypeDeclaration cla /** * create a sort out of a recoder class * - * @param ct classtype to create for, not null + * @param ct classtype to create for, not null * @param supers the set of (direct?) super-sorts * @return a freshly created Sort object */ @@ -326,13 +330,13 @@ private ArrayDeclaration createArrayType(KeYJavaType baseType, KeYJavaType array baseTypeRef = new TypeRef(baseType); } else { baseTypeRef = new TypeRef(new ProgramElementName(baseType.getSort().name().toString()), - 0, null, baseType); + 0, null, baseType); } ExtList members = new ExtList(); members.add(baseTypeRef); addImplicitArrayMembers(members, arrayType, baseType, - (ProgramVariable) length.getFieldSpecifications().get(0).getProgramVariable()); + (ProgramVariable) length.getFieldSpecifications().get(0).getProgramVariable()); return new ArrayDeclaration(members, baseTypeRef, sat); } @@ -348,10 +352,10 @@ private KeYJavaType createSuperArrayType() { var superArrayType = new KeYJavaType(); var specLength = - new FieldSpecification(new LocationVariable(new ProgramElementName("length"), - integerType, superArrayType, false, false, false, true)); - var f = new FieldDeclaration(new Modifier[] { new Public(), new Final() }, - new TypeRef(integerType), new FieldSpecification[] { specLength }, false); + new FieldSpecification(new LocationVariable(new ProgramElementName("length"), + integerType, superArrayType, false, false, false, true)); + var f = new FieldDeclaration(new Modifier[]{new Public(), new Final()}, + new TypeRef(integerType), new FieldSpecification[]{specLength}, false); superArrayType.setJavaType(new SuperArrayDeclaration(f)); return superArrayType; } @@ -359,18 +363,18 @@ private KeYJavaType createSuperArrayType() { /** * Adds several implicit fields and methods to given list of members. * - * @param members an ExtList with the members of parent - * @param parent the KeYJavaType of the array to be enriched by its implicit members + * @param members an ExtList with the members of parent + * @param parent the KeYJavaType of the array to be enriched by its implicit members * @param baseType the KeYJavaType of the parent's element type */ private void addImplicitArrayMembers(ExtList members, KeYJavaType parent, KeYJavaType baseType, - ProgramVariable len) { + ProgramVariable len) { Type base = baseType.getJavaType(); int dimension = base instanceof ArrayType ? ((ArrayType) base).getDimension() + 1 : 1; TypeRef parentReference = - new TypeRef(new ProgramElementName(String.valueOf(parent.getSort().name())), - dimension, null, parent); + new TypeRef(new ProgramElementName(String.valueOf(parent.getSort().name())), + dimension, null, parent); // add methods // the only situation where base can be null is in case of a @@ -386,7 +390,7 @@ private void addImplicitArrayMembers(ExtList members, KeYJavaType parent, KeYJav } final IProgramMethod prepare = - arrayMethodBuilder.getPrepareArrayMethod(parentReference, length, defaultValue, fields); + arrayMethodBuilder.getPrepareArrayMethod(parentReference, length, defaultValue, fields); members.add(arrayMethodBuilder.getArrayInstanceAllocatorMethod(parentReference)); members.add(prepare); @@ -399,7 +403,7 @@ private void addImplicitArrayMembers(ExtList members, KeYJavaType parent, KeYJav * * @param field the FieldDeclaration of which the field specifications have to be extracted * @return a IList the includes all field specifications found int the field declaration - * of the given list + * of the given list */ private ImmutableList filterField(FieldDeclaration field) { ImmutableList result = ImmutableSLList.nil(); @@ -416,7 +420,7 @@ private ImmutableList filterField(FieldDeclaration field) { * * @param list the ExtList with the members of a type declaration * @return a IList the includes all field specifications found int the field declaration - * of the given list + * of the given list */ private ImmutableList filterField(ExtList list) { ImmutableList result = ImmutableSLList.nil(); @@ -435,6 +439,6 @@ private void initArrayMethodBuilder() { Sort heapSort = heapLDT == null ? Sort.ANY : heapLDT.targetSort(); int heapCount = (heapLDT == null) ? 1 : (heapLDT.getAllHeaps().size() - 1); arrayMethodBuilder = - new CreateArrayMethodBuilder(integerType, getObjectType(), heapSort, heapCount); + new CreateArrayMethodBuilder(integerType, getObjectType(), heapSort, heapCount); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstructorCall.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstructorCall.java index a38683df326..867911ede52 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstructorCall.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstructorCall.java @@ -100,7 +100,8 @@ protected List constructorCallSequence(final New constructorReference final KeYJavaType classType, SVInstantiations svInst, Services services) { assert (newObjectVar == null) != (newObjectSV == null); - final ProgramVariable newObject = newObjectSV == null ? newObjectVar + final ProgramVariable newObject = newObjectSV == null + ? newObjectVar : (ProgramVariable) svInst.getInstantiation(newObjectSV); final ExecutionContext ec = svInst.getExecutionContext(); final ImmutableArray arguments = constructorReference.getArguments(); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java index 2e1a650dca8..a8ece15f564 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java @@ -43,12 +43,12 @@ public class ProveTest { protected final boolean verbose = Boolean.getBoolean("prooftests.verbose"); protected String baseDirectory = ""; - protected final String statisticsFile = "tmp.csv"; + protected String statisticsFile = "tmp.csv"; protected String name = "unnamed_tests"; - protected final boolean reloadEnabled = false; + protected boolean reloadEnabled = false; protected String tempDir = "/tmp"; - protected final String globalSettings = ""; - protected final String localSettings = ""; + protected String globalSettings = ""; + protected String localSettings = ""; private StatisticsFile statistics; protected void assertProvability(String file) throws Exception {