Skip to content

Commit 0a20b91

Browse files
unp1unp1
committed
Remove mutable list from AST
1 parent ddec097 commit 0a20b91

19 files changed

Lines changed: 110 additions & 111 deletions

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818

1919
import org.key_project.logic.IntIterator;
2020
import org.key_project.util.collection.ImmutableArray;
21+
import org.key_project.util.collection.ImmutableSLList;
2122

2223
/**
2324
* In the DL-formulae description of Taclets the program part can have the following form
@@ -51,7 +52,7 @@ public ContextStatementBlock(
5152
PositionInfo pi, List<Comment> c,
5253
ImmutableArray<? extends Statement> body,
5354
IExecutionContext execContext) {
54-
super(pi, c, body);
55+
super(pi, c, body, ImmutableSLList.nil());
5556
this.executionContext = execContext;
5657
}
5758

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/ProgramElement.java‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,13 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.java.ast;
55

6-
import java.util.List;
76

87
import de.uka.ilkd.key.rule.MatchConditions;
98
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
109

10+
import org.key_project.util.collection.ImmutableList;
11+
import org.key_project.util.collection.ImmutableSLList;
12+
1113
import org.jspecify.annotations.Nullable;
1214

1315
/**
@@ -25,8 +27,8 @@ public interface ProgramElement extends SourceElement, ModelElement {
2527
Comment[] getComments();
2628

2729
///
28-
default List<TextualJMLConstruct> getAttachedJml() {
29-
return List.of();
30+
default ImmutableList<TextualJMLConstruct> getAttachedJml() {
31+
return ImmutableSLList.nil();
3032
}
3133

3234

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java‎

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

66
import java.util.ArrayList;
7+
import java.util.Arrays;
78
import java.util.List;
89

910
import de.uka.ilkd.key.java.Position;
@@ -20,6 +21,8 @@
2021

2122
import org.key_project.util.ExtList;
2223
import org.key_project.util.collection.ImmutableArray;
24+
import org.key_project.util.collection.ImmutableList;
25+
import org.key_project.util.collection.ImmutableSLList;
2326

2427
import org.jspecify.annotations.NonNull;
2528
import org.jspecify.annotations.Nullable;
@@ -40,22 +43,25 @@ public class StatementBlock extends JavaStatement implements StatementContainer,
4043

4144
@Nullable
4245
private final MethodFrame innerMostMethodFrame;
43-
private final List<TextualJMLConstruct> attachedJML = new ArrayList<>(0);
46+
private final ImmutableList<TextualJMLConstruct> attachedJML;
4447

4548
public StatementBlock(
4649
PositionInfo pi, List<Comment> comments,
47-
@NonNull ImmutableArray<? extends Statement> body) {
50+
@NonNull ImmutableArray<? extends Statement> body,
51+
ImmutableList<TextualJMLConstruct> attachedJML) {
4852
super(pi, comments);
4953
this.body = body;
5054
ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this);
5155
prefixLength = info.getLength();
5256
innerMostMethodFrame = info.getInnerMostMethodFrame();
57+
this.attachedJML = attachedJML;
5358
}
5459

5560
public StatementBlock() {
5661
body = new ImmutableArray<>();
5762
prefixLength = 1;
5863
innerMostMethodFrame = null;
64+
attachedJML = ImmutableList.of();
5965
}
6066

6167

@@ -71,6 +77,8 @@ public StatementBlock(ExtList children) {
7177
ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this);
7278
prefixLength = info.getLength();
7379
innerMostMethodFrame = info.getInnerMostMethodFrame();
80+
attachedJML =
81+
ImmutableList.fromList(Arrays.asList(children.collect(TextualJMLConstruct.class)));
7482
}
7583

7684
public StatementBlock(@NonNull ImmutableArray<? extends Statement> as) {
@@ -81,6 +89,7 @@ public StatementBlock(@NonNull ImmutableArray<? extends Statement> as) {
8189
ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this);
8290
prefixLength = info.getLength();
8391
innerMostMethodFrame = info.getInnerMostMethodFrame();
92+
attachedJML = ImmutableSLList.nil();
8493
}
8594

8695

@@ -94,12 +103,11 @@ public StatementBlock(Statement... body) {
94103

95104
public StatementBlock(PositionInfo pi, List<Comment> c, ImmutableArray<Statement> body,
96105
List<TextualJMLConstruct> spec) {
97-
this(pi, c, body);
98-
attachedJML.addAll(spec);
106+
this(pi, c, body, ImmutableList.fromList(spec));
99107
}
100108

101109
@Override
102-
public List<TextualJMLConstruct> getAttachedJml() {
110+
public ImmutableList<TextualJMLConstruct> getAttachedJml() {
103111
return attachedJML;
104112
}
105113

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java‎

Lines changed: 4 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -121,27 +121,17 @@ public ClassDeclaration(PositionInfo pi, List<Comment> c, ImmutableArray<Modifie
121121
ProgramElementName name, ProgramElementName fullName,
122122
ImmutableArray<MemberDeclaration> members, boolean parentIsInterface,
123123
boolean isLibrary, Extends extending, Implements implementing, boolean innerClass,
124-
boolean localClassDeclaration, boolean isAnonymousClass) {
125-
super(pi, c, modArray, name, fullName, members, parentIsInterface, isLibrary);
124+
boolean localClassDeclaration, boolean isAnonymousClass,
125+
ImmutableList<TextualJMLConstruct> spec) {
126+
super(pi, c, modArray, name, fullName, members, parentIsInterface, isLibrary,
127+
ImmutableList.fromList(spec));
126128
this.extending = extending;
127129
this.implementing = implementing;
128130
this.isInnerClass = innerClass;
129131
this.isLocalClass = localClassDeclaration;
130132
this.isAnonymousClass = isAnonymousClass;
131133
}
132134

133-
public ClassDeclaration(PositionInfo pi, List<Comment> c, ImmutableArray<Modifier> modArray,
134-
ProgramElementName name, ProgramElementName fullName,
135-
ImmutableArray<MemberDeclaration> members,
136-
boolean parentIsInterface, boolean isLibrary, Extends extending,
137-
Implements implementing,
138-
boolean innerClass, boolean localClassDeclaration, boolean isAnonymousClass,
139-
List<TextualJMLConstruct> spec) {
140-
this(pi, c, modArray, name, fullName, members, parentIsInterface, isLibrary, extending,
141-
implementing, innerClass,
142-
localClassDeclaration, isAnonymousClass);
143-
attachedJml.addAll(spec);
144-
}
145135

146136

147137
/**

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ConstructorDeclaration.java‎

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616

1717
import org.key_project.util.ExtList;
1818
import org.key_project.util.collection.ImmutableArray;
19+
import org.key_project.util.collection.ImmutableList;
1920

2021

2122
/**
@@ -58,20 +59,13 @@ public ConstructorDeclaration(Modifier[] modifiers, ProgramElementName name,
5859
super(modifiers, null, name, parameters, exceptions, body, parentIsInterfaceDeclaration);
5960
}
6061

61-
public ConstructorDeclaration(PositionInfo pi, List<Comment> c, ImmutableArray<Modifier> map,
62-
TypeReference o, Comment[] comments, ProgramElementName name,
63-
ImmutableArray<ParameterDeclaration> map1,
64-
Throws exceptions, StatementBlock body, boolean parentIsInterfaceDeclaration) {
65-
super(pi, c, map, o, comments, name, map1, exceptions, body, parentIsInterfaceDeclaration);
66-
}
67-
6862
public ConstructorDeclaration(PositionInfo pi, List<Comment> c, ImmutableArray<Modifier> map,
6963
TypeReference o, Comment[] comments, ProgramElementName name,
7064
ImmutableArray<ParameterDeclaration> map1,
7165
Throws exceptions, StatementBlock body, boolean parentIsInterfaceDeclaration,
7266
List<TextualJMLConstruct> specs) {
73-
this(pi, c, map, o, comments, name, map1, exceptions, body, parentIsInterfaceDeclaration);
74-
attachedJml.addAll(specs);
67+
super(pi, c, map, o, comments, name, map1, exceptions, body, parentIsInterfaceDeclaration,
68+
ImmutableList.fromList(specs));
7569
}
7670

7771
/**

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InterfaceDeclaration.java‎

Lines changed: 3 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -43,9 +43,10 @@ public class InterfaceDeclaration extends TypeDeclaration {
4343
public InterfaceDeclaration(PositionInfo pi, List<Comment> comments,
4444
@NonNull ImmutableArray<Modifier> modArray, ProgramElementName name,
4545
ProgramElementName fullName, ImmutableArray<MemberDeclaration> members,
46-
boolean parentIsInterfaceDeclaration, boolean isLibrary, Extends extending) {
46+
boolean parentIsInterfaceDeclaration, boolean isLibrary, Extends extending,
47+
List<TextualJMLConstruct> spec) {
4748
super(pi, comments, modArray, name, fullName, members, parentIsInterfaceDeclaration,
48-
isLibrary);
49+
isLibrary, ImmutableList.fromList(spec));
4950
this.extending = extending;
5051
}
5152

@@ -102,16 +103,6 @@ public InterfaceDeclaration(ProgramElementName name) {
102103
true);
103104
}
104105

105-
public InterfaceDeclaration(PositionInfo pi, List<Comment> c, ImmutableArray<Modifier> modArray,
106-
ProgramElementName name, ProgramElementName fullName,
107-
ImmutableArray<MemberDeclaration> members,
108-
boolean parentIsInterface, boolean isLibrary, Extends extending,
109-
List<TextualJMLConstruct> spec) {
110-
this(pi, c, modArray, name, fullName, members, parentIsInterface, isLibrary, extending);
111-
attachedJml.addAll(spec);
112-
}
113-
114-
115106
/**
116107
* Returns the number of children of this node.
117108
*

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/JavaDeclaration.java‎

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,6 @@
1616

1717
package de.uka.ilkd.key.java.ast.declaration;
1818

19-
import java.util.ArrayList;
20-
import java.util.Collections;
2119
import java.util.List;
2220

2321
import de.uka.ilkd.key.java.ast.Comment;
@@ -29,6 +27,8 @@
2927

3028
import org.key_project.util.ExtList;
3129
import org.key_project.util.collection.ImmutableArray;
30+
import org.key_project.util.collection.ImmutableList;
31+
import org.key_project.util.collection.ImmutableSLList;
3232

3333
import org.jspecify.annotations.NonNull;
3434

@@ -38,17 +38,9 @@
3838
*/
3939

4040
public abstract class JavaDeclaration extends JavaNonTerminalProgramElement implements Declaration {
41-
protected final List<TextualJMLConstruct> attachedJml = new ArrayList<>();
4241

43-
@Override
44-
public List<TextualJMLConstruct> getAttachedJml() {
45-
return Collections.unmodifiableList(attachedJml);
46-
}
42+
protected final ImmutableList<TextualJMLConstruct> attachedJml;
4743

48-
@Override
49-
public @NonNull ImmutableArray<Modifier> getModifiers() {
50-
return modArray;
51-
}
5244

5345
/**
5446
* Modifiers.
@@ -60,26 +52,28 @@ public List<TextualJMLConstruct> getAttachedJml() {
6052
protected final ImmutableArray<Modifier> modArray;
6153

6254
public JavaDeclaration(PositionInfo pi, List<Comment> comments,
63-
@NonNull ImmutableArray<Modifier> modArray) {
55+
@NonNull ImmutableArray<Modifier> modArray,
56+
ImmutableList<TextualJMLConstruct> attachedJml) {
6457
super(pi, comments);
6558
this.modArray = modArray;
59+
this.attachedJml = attachedJml;
6660
}
6761

6862
/**
6963
* Java declaration.
7064
*/
7165
public JavaDeclaration() {
72-
this(null, null, new ImmutableArray<>());
66+
this(null, null, new ImmutableArray<>(), ImmutableSLList.nil());
7367
}
7468

7569

7670
public JavaDeclaration(Modifier[] mods) {
77-
this(null, null, new ImmutableArray<>(mods));
71+
this(null, null, new ImmutableArray<>(mods), ImmutableSLList.nil());
7872
}
7973

8074

8175
public JavaDeclaration(ImmutableArray<Modifier> mods) {
82-
this(null, null, mods);
76+
this(null, null, mods, ImmutableSLList.nil());
8377
}
8478

8579

@@ -94,6 +88,8 @@ public JavaDeclaration(ImmutableArray<Modifier> mods) {
9488
public JavaDeclaration(ExtList children) {
9589
super(children);
9690
modArray = new ImmutableArray<>(children.collect(Modifier.class));
91+
this.attachedJml =
92+
ImmutableList.fromList(List.of(children.collect(TextualJMLConstruct.class)));
9793
}
9894

9995

@@ -112,6 +108,16 @@ public VisibilityModifier getVisibilityModifier() {
112108
return null;
113109
}
114110

111+
@Override
112+
public @NonNull ImmutableArray<Modifier> getModifiers() {
113+
return modArray;
114+
}
115+
116+
117+
@Override
118+
public ImmutableList<TextualJMLConstruct> getAttachedJml() {
119+
return attachedJml;
120+
}
115121

116122
public boolean containsModifier(Class<?> type) {
117123
int s = modArray.size();

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java‎

Lines changed: 4 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818

1919
import org.key_project.util.ExtList;
2020
import org.key_project.util.collection.ImmutableArray;
21+
import org.key_project.util.collection.ImmutableList;
2122

2223
import org.jspecify.annotations.NonNull;
2324

@@ -92,8 +93,9 @@ public MethodDeclaration(
9293
TypeReference returnType,
9394
Comment[] voidComments, ProgramElementName name,
9495
ImmutableArray<ParameterDeclaration> parameters, Throws exceptions,
95-
StatementBlock body, boolean parentIsInterfaceDeclaration) {
96-
super(pi, comments, modArray);
96+
StatementBlock body, boolean parentIsInterfaceDeclaration,
97+
ImmutableList<TextualJMLConstruct> attachedJml) {
98+
super(pi, comments, modArray, attachedJml);
9799
this.returnType = returnType;
98100
this.voidComments = voidComments;
99101
this.name = name;
@@ -104,18 +106,6 @@ public MethodDeclaration(
104106
this.jmlModifiers = JMLInfoExtractor.parseMethod(this);
105107
}
106108

107-
public MethodDeclaration(
108-
PositionInfo pi, List<Comment> comments,
109-
@NonNull ImmutableArray<Modifier> modArray,
110-
TypeReference returnType,
111-
Comment[] voidComments, ProgramElementName name,
112-
ImmutableArray<ParameterDeclaration> parameters, Throws exceptions,
113-
StatementBlock body, boolean parentIsInterfaceDeclaration,
114-
List<TextualJMLConstruct> specs) {
115-
this(pi, comments, modArray, returnType, voidComments, name, parameters, exceptions,
116-
body, parentIsInterfaceDeclaration);
117-
attachedJml.addAll(specs);
118-
}
119109

120110
/**
121111
* Method declaration.

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
import de.uka.ilkd.key.java.ast.expression.literal.NullLiteral;
1313
import de.uka.ilkd.key.logic.ProgramElementName;
1414
import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor;
15+
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
1516
import de.uka.ilkd.key.speclang.njml.SpecMathMode;
1617

1718
import org.key_project.util.ExtList;
@@ -62,8 +63,8 @@ public TypeDeclaration(
6263
@NonNull ImmutableArray<Modifier> modArray,
6364
ProgramElementName name, ProgramElementName fullName,
6465
ImmutableArray<MemberDeclaration> members, boolean parentIsInterfaceDeclaration,
65-
boolean isLibrary) {
66-
super(pi, comments, modArray);
66+
boolean isLibrary, ImmutableList<TextualJMLConstruct> jmlAttachments) {
67+
super(pi, comments, modArray, jmlAttachments);
6768
this.name = name;
6869
this.fullName = fullName;
6970
this.members = members;

‎key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/VariableDeclaration.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414

1515
import org.key_project.util.ExtList;
1616
import org.key_project.util.collection.ImmutableArray;
17+
import org.key_project.util.collection.ImmutableSLList;
1718

1819
import org.jspecify.annotations.NonNull;
1920

@@ -101,7 +102,7 @@ protected VariableDeclaration(ExtList children, boolean parentIsInterfaceDeclara
101102

102103
public VariableDeclaration(PositionInfo pi, List<Comment> c, ImmutableArray<Modifier> modArray,
103104
TypeReference type, boolean parentIsInferface) {
104-
super(pi, c, modArray);
105+
super(pi, c, modArray, ImmutableSLList.nil());
105106
this.typeReference = type;
106107
this.parentIsInterfaceDeclaration = parentIsInferface;
107108
}

0 commit comments

Comments
 (0)