Skip to content

Commit 9a215ec

Browse files
committed
fix DocSpace parentship
1 parent 95670bb commit 9a215ec

3 files changed

Lines changed: 18 additions & 8 deletions

File tree

key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.ldt;
55

6+
import java.util.Objects;
7+
68
import de.uka.ilkd.key.proof.init.InitConfig;
79
import de.uka.ilkd.key.settings.ProofSettings;
810

@@ -51,8 +53,8 @@ public static boolean isFinalEnabled(@NonNull InitConfig initConfig) {
5153
* @return true if final fields are treated as immutable
5254
*/
5355
public static boolean isFinalEnabled(@NonNull ProofSettings settings) {
54-
return settings.getChoiceSettings().getDefaultChoices().get(SETTING)
55-
.equals(IMMUTABLE_OPTION);
56+
return Objects.equals(settings.getChoiceSettings().getDefaultChoices().get(SETTING),
57+
IMMUTABLE_OPTION);
5658
}
5759

5860
/**

key.core/src/main/java/de/uka/ilkd/key/logic/DocSpace.java

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,11 @@ public DocSpace(DocSpace parent) {
2626
this.parent = parent;
2727
}
2828

29+
public DocSpace(@Nullable DocSpace parent, Map<String, String> documentation) {
30+
this(documentation);
31+
this.parent = parent;
32+
}
33+
2934
public @Nullable String find(String key) {
3035
var value = documentation.get(key);
3136
if (value != null)
@@ -59,6 +64,6 @@ public void describe(HasDocumentation entity, @Nullable String doc) {
5964
}
6065

6166
public DocSpace copy() {
62-
return new DocSpace(documentation);
67+
return new DocSpace(parent, documentation);
6368
}
6469
}

key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@
44
package de.uka.ilkd.key.logic;
55

66

7+
import java.util.Objects;
8+
79
import de.uka.ilkd.key.logic.op.IProgramVariable;
810
import org.jspecify.annotations.NullMarked;
911
import de.uka.ilkd.key.logic.op.ParametricFunctionDecl;
@@ -32,7 +34,7 @@ public class NamespaceSet {
3234
private Namespace<ParametricSortDecl> parametricSortNS = new Namespace<>();
3335
private Namespace<ParametricFunctionDecl> parametricFuncNS = new Namespace<>();
3436
private Namespace<Choice> choiceNS = new Namespace<>();
35-
private final DocSpace documentation = new DocSpace();
37+
private DocSpace documentation = new DocSpace();
3638

3739
public NamespaceSet() {
3840
}
@@ -65,7 +67,7 @@ public NamespaceSet(Namespace<QuantifiableVariable> varNS,
6567
this.choiceNS = choiceNS;
6668
this.parametricSortNS = parametricSortNS;
6769
this.parametricFuncNS = parametricFuncNS;
68-
this.documentation.add(documentation);
70+
this.documentation = Objects.requireNonNull(documentation);
6971
}
7072

7173

@@ -89,7 +91,8 @@ public NamespaceSet copyWithParent() {
8991
new Namespace<>(functions()), new Namespace<>(sorts()),
9092
new Namespace<>(ruleSets()), new Namespace<>(parametricSorts()),
9193
new Namespace<>(parametricFunctions()), new Namespace<>(choices()),
92-
new Namespace<>(programVariables()));
94+
new Namespace<>(programVariables()),
95+
new DocSpace(documentation));
9396
}
9497

9598
public Namespace<QuantifiableVariable> variables() {
@@ -258,13 +261,13 @@ public boolean isEmpty() {
258261
public NamespaceSet simplify() {
259262
return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(),
260263
ruleSetNS.simplify(), parametricSortNS.simplify(), parametricFuncNS.simplify(),
261-
choiceNS.simplify(), progVarNS.simplify());
264+
choiceNS.simplify(), progVarNS.simplify(), documentation);
262265
}
263266

264267
public NamespaceSet getCompression() {
265268
return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(),
266269
ruleSetNS.compress(), parametricSortNS.compress(), parametricFuncNS.compress(),
267-
choiceNS.compress(), progVarNS.compress());
270+
choiceNS.compress(), progVarNS.compress(), documentation);
268271
}
269272

270273
public void flushToParent() {

0 commit comments

Comments
 (0)