Skip to content

Commit beed211

Browse files
committed
Fix potential wrong usage of ProgramElementName constructor
1 parent ab78513 commit beed211

3 files changed

Lines changed: 8 additions & 3 deletions

File tree

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1281,6 +1281,7 @@ private ProgramVariable getProgramVariableForFieldSpecification(
12811281
Type recoderType =
12821282
(getServiceConfiguration().getSourceInfo()).getType(recoderVarSpec);
12831283
final ClassType recContainingClassType = recoderVarSpec.getContainingClassType();
1284+
12841285
final ProgramElementName pen =
12851286
new ProgramElementName(makeAdmissibleName(recoderVarSpec.getName()),
12861287
makeAdmissibleName(recContainingClassType.getFullName()));

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,10 @@ public void check(Services javaServ, KeYJavaType containingClass) throws Convert
106106
String qualifier =
107107
name.lastIndexOf('.') != -1 ? name.substring(0, name.lastIndexOf('.')) : "";
108108
name = name.substring(name.lastIndexOf('.') + 1);
109-
TypeRef tr = new TypeRef(new ProgramElementName(name, qualifier), 0, null, containingClass);
109+
final ProgramElementName programName =
110+
qualifier.isEmpty() ? new ProgramElementName(name)
111+
: new ProgramElementName(name, qualifier);
112+
TypeRef tr = new TypeRef(programName, 0, null, containingClass);
110113
ExecutionContext ec = new ExecutionContext(tr, null, null);
111114

112115
for (int i = 0; i < actual; i++) {

key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,6 @@
4242
import de.uka.ilkd.key.strategy.StrategyProperties;
4343
import de.uka.ilkd.key.util.KeYConstants;
4444

45-
import org.jspecify.annotations.NonNull;
4645
import org.key_project.logic.Name;
4746
import org.key_project.logic.PosInTerm;
4847
import org.key_project.logic.op.Modality;
@@ -59,6 +58,7 @@
5958
import org.key_project.util.collection.ImmutableList;
6059
import org.key_project.util.collection.ImmutableMapEntry;
6160

61+
import org.jspecify.annotations.NonNull;
6262
import org.jspecify.annotations.Nullable;
6363
import org.slf4j.Logger;
6464
import org.slf4j.LoggerFactory;
@@ -678,7 +678,8 @@ public static String posInTerm2Proof(PosInTerm pos) {
678678
public Collection<String> getInterestingInstantiations(SVInstantiations inst) {
679679
Collection<String> s = new ArrayList<>();
680680

681-
for (final ImmutableMapEntry<@NonNull SchemaVariable, @NonNull InstantiationEntry<?>> pair : inst.interesting()) {
681+
for (final ImmutableMapEntry<@NonNull SchemaVariable, @NonNull InstantiationEntry<?>> pair : inst
682+
.interesting()) {
682683
final SchemaVariable var = pair.key();
683684

684685
final Object value = pair.value().getInstantiation();

0 commit comments

Comments
 (0)