Skip to content

Commit f006f35

Browse files
unp1wadoon
authored andcommitted
Fix potential wrong usage of ProgramElementName constructor
1 parent aaf4b99 commit f006f35

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
@@ -44,7 +44,6 @@
4444
import de.uka.ilkd.key.strategy.StrategyProperties;
4545
import de.uka.ilkd.key.util.KeYConstants;
4646

47-
import org.jspecify.annotations.NonNull;
4847
import org.key_project.logic.Name;
4948
import org.key_project.logic.PosInTerm;
5049
import org.key_project.logic.op.Modality;
@@ -61,6 +60,7 @@
6160
import org.key_project.util.collection.ImmutableList;
6261
import org.key_project.util.collection.ImmutableMapEntry;
6362

63+
import org.jspecify.annotations.NonNull;
6464
import org.jspecify.annotations.Nullable;
6565
import org.slf4j.Logger;
6666
import org.slf4j.LoggerFactory;
@@ -680,7 +680,8 @@ public static String posInTerm2Proof(PosInTerm pos) {
680680
public Collection<String> getInterestingInstantiations(SVInstantiations inst) {
681681
Collection<String> s = new ArrayList<>();
682682

683-
for (final ImmutableMapEntry<@NonNull SchemaVariable, @NonNull InstantiationEntry<?>> pair : inst.interesting()) {
683+
for (final ImmutableMapEntry<@NonNull SchemaVariable, @NonNull InstantiationEntry<?>> pair : inst
684+
.interesting()) {
684685
final SchemaVariable var = pair.key();
685686

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

0 commit comments

Comments
 (0)