From b41c2b79ffd3b3b068fea3f3a8e3ba22d4d9b6b3 Mon Sep 17 00:00:00 2001
From: Drodt
Date: Wed, 27 Mar 2024 08:53:50 +0100
Subject: [PATCH 01/11] API design
---
.../org/key_project/logic/SyntaxElement.java | 3 +++
.../logic/SyntaxElementCursor.java | 23 +++++++++++++++++++
.../logic/SyntaxElementCursorNode.java | 4 ++++
3 files changed, 30 insertions(+)
create mode 100644 key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java
create mode 100644 key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursorNode.java
diff --git a/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java b/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java
index 244f53bbe4b..347ec52dd1b 100644
--- a/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java
+++ b/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java
@@ -8,4 +8,7 @@
* AST nodes.
*/
public interface SyntaxElement {
+ SyntaxElement getChild(int child);
+
+ int getChildCount();
}
diff --git a/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java
new file mode 100644
index 00000000000..ee6ad7d01ee
--- /dev/null
+++ b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java
@@ -0,0 +1,23 @@
+package org.key_project.logic;
+
+public class SyntaxElementCursor {
+ public SyntaxElement getCurrentNode() {
+ return null;
+ }
+
+ public SyntaxElementCursorNode getCurrentTreeCursorNode() {
+ return null;
+ }
+
+ public boolean gotoFirstChild() {
+ return false;
+ }
+
+ public boolean gotoNextSibling() {
+ return false;
+ }
+
+ public boolean gotoParent() {
+ return false;
+ }
+}
diff --git a/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursorNode.java b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursorNode.java
new file mode 100644
index 00000000000..f6494c6efd3
--- /dev/null
+++ b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursorNode.java
@@ -0,0 +1,4 @@
+package org.key_project.logic;
+
+public record SyntaxElementCursorNode(String type, String name) {
+}
From 179d71e8b65e1f357cbb6774fd71703a203b1da7 Mon Sep 17 00:00:00 2001
From: Drodt
Date: Thu, 2 May 2024 10:18:09 +0200
Subject: [PATCH 02/11] Increase Java version
---
gradle/wrapper/gradle-wrapper.properties | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties
index e411586a54a..48c0a02ca41 100644
--- a/gradle/wrapper/gradle-wrapper.properties
+++ b/gradle/wrapper/gradle-wrapper.properties
@@ -1,5 +1,5 @@
distributionBase=GRADLE_USER_HOME
distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip
zipStoreBase=GRADLE_USER_HOME
zipStorePath=wrapper/dists
From c168bb765ca93673a929ceff446abd852882c990 Mon Sep 17 00:00:00 2001
From: Drodt
Date: Thu, 2 May 2024 11:08:10 +0200
Subject: [PATCH 03/11] Implement cursor
---
.../org/key_project/logic/SyntaxElement.java | 12 +++++-
.../logic/SyntaxElementCursor.java | 37 +++++++++++++++----
.../logic/SyntaxElementCursorNode.java | 4 --
3 files changed, 41 insertions(+), 12 deletions(-)
delete mode 100644 key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursorNode.java
diff --git a/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java b/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java
index 347ec52dd1b..a9e2a7e0bd0 100644
--- a/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java
+++ b/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java
@@ -8,7 +8,17 @@
* AST nodes.
*/
public interface SyntaxElement {
- SyntaxElement getChild(int child);
+ /**
+ * Get the {@code n}-th child of this syntax element.
+ * @param n index of the child.
+ * @return the {@code n}-th child of this syntax element.
+ * @throws IndexOutOfBoundsException if there is no {@code n}-th child.
+ */
+ SyntaxElement getChild(int n);
+ /**
+ *
+ * @return the number of children of this syntax element.
+ */
int getChildCount();
}
diff --git a/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java
index ee6ad7d01ee..fdc3e6013cd 100644
--- a/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java
+++ b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java
@@ -1,23 +1,46 @@
package org.key_project.logic;
+import java.util.ArrayDeque;
+import java.util.Deque;
+
public class SyntaxElementCursor {
- public SyntaxElement getCurrentNode() {
- return null;
+ record ParentAndPosition(SyntaxElement parent, int index) {}
+
+ private final Deque path = new ArrayDeque<>();
+
+ private SyntaxElement node;
+
+ SyntaxElementCursor(SyntaxElement node) {
+ this.node = node;
}
- public SyntaxElementCursorNode getCurrentTreeCursorNode() {
- return null;
+ public SyntaxElement getCurrentNode() {
+ return node;
}
public boolean gotoFirstChild() {
- return false;
+ if (node.getChildCount() <= 0) return false;
+ path.push(new ParentAndPosition(node, 0));
+ node = node.getChild(0);
+ return true;
}
public boolean gotoNextSibling() {
- return false;
+ if (path.isEmpty()) return false;
+ var pnp = path.pop();
+ SyntaxElement parent = pnp.parent;
+ int index =pnp.index+1;
+ if (index > parent.getChildCount()) {
+ return false;
+ }
+ path.push(new ParentAndPosition(parent, index));
+ node = parent.getChild(index);
+ return true;
}
public boolean gotoParent() {
- return false;
+ if (path.isEmpty()) return false;
+ node = path.pop().parent;
+ return true;
}
}
diff --git a/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursorNode.java b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursorNode.java
deleted file mode 100644
index f6494c6efd3..00000000000
--- a/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursorNode.java
+++ /dev/null
@@ -1,4 +0,0 @@
-package org.key_project.logic;
-
-public record SyntaxElementCursorNode(String type, String name) {
-}
From fe83fc86efccd3fa093e919886202e0718c1fa53 Mon Sep 17 00:00:00 2001
From: Drodt
Date: Wed, 8 May 2024 13:47:00 +0200
Subject: [PATCH 04/11] Start implementation of traversal
---
.../MethodCallProofReferencesAnalyst.java | 2 +-
.../ProgramVariableReferencesAnalyst.java | 2 +-
.../slicing/AbstractBackwardSlicer.java | 2 +-
.../slicing/AbstractSlicer.java | 2 +-
.../breakpoint/ExceptionBreakpoint.java | 2 +-
.../strategy/breakpoint/FieldWatchpoint.java | 4 +-
.../SymbolicExecutionExceptionBreakpoint.java | 2 +-
.../util/SymbolicExecutionUtil.java | 4 +-
.../CcatchBreakLabelParameterDeclaration.java | 2 +-
.../java/CcatchBreakParameterDeclaration.java | 2 +-
...atchBreakWildcardParameterDeclaration.java | 2 +-
...atchContinueLabelParameterDeclaration.java | 2 +-
.../CcatchContinueParameterDeclaration.java | 2 +-
...hContinueWildcardParameterDeclaration.java | 2 +-
.../CcatchReturnParameterDeclaration.java | 2 +-
.../CcatchReturnValParameterDeclaration.java | 2 +-
.../java/de/uka/ilkd/key/java/Comment.java | 12 ++++++
.../de/uka/ilkd/key/java/CompilationUnit.java | 6 +--
.../ilkd/key/java/ContextStatementBlock.java | 4 +-
.../java/de/uka/ilkd/key/java/Import.java | 2 +-
.../java/JavaNonTerminalProgramElement.java | 16 +++++---
.../key/java/NonTerminalProgramElement.java | 2 +-
.../ilkd/key/java/PackageSpecification.java | 2 +-
.../java/de/uka/ilkd/key/java/SourceData.java | 2 +-
.../de/uka/ilkd/key/java/SourceElement.java | 4 +-
.../de/uka/ilkd/key/java/StatementBlock.java | 2 +-
.../ilkd/key/java/TerminalProgramElement.java | 11 +++++
.../java/declaration/ArrayDeclaration.java | 2 +-
.../java/declaration/ClassDeclaration.java | 2 +-
.../java/declaration/ClassInitializer.java | 2 +-
.../java/declaration/FieldDeclaration.java | 2 +-
.../declaration/InheritanceSpecification.java | 2 +-
.../declaration/InterfaceDeclaration.java | 2 +-
.../declaration/LocalVariableDeclaration.java | 2 +-
.../java/declaration/MethodDeclaration.java | 4 +-
.../declaration/ParameterDeclaration.java | 2 +-
.../declaration/SuperArrayDeclaration.java | 2 +-
.../uka/ilkd/key/java/declaration/Throws.java | 2 +-
.../java/declaration/VariableDeclaration.java | 2 +-
.../declaration/VariableSpecification.java | 6 +--
.../modifier/AnnotationUseSpecification.java | 2 +-
.../key/java/expression/ArrayInitializer.java | 2 +-
.../ilkd/key/java/expression/Operator.java | 2 +-
.../expression/operator/ExactInstanceof.java | 2 +-
.../java/expression/operator/Instanceof.java | 6 +--
.../key/java/expression/operator/New.java | 4 +-
.../java/expression/operator/NewArray.java | 2 +-
.../java/expression/operator/TypeCast.java | 2 +-
.../java/reference/ArrayLengthReference.java | 2 +-
.../key/java/reference/ArrayReference.java | 2 +-
.../key/java/reference/ExecutionContext.java | 2 +-
.../key/java/reference/FieldReference.java | 2 +-
.../java/reference/MetaClassReference.java | 2 +-
.../key/java/reference/MethodReference.java | 2 +-
.../key/java/reference/PackageReference.java | 2 +-
.../reference/SchematicFieldReference.java | 2 +-
.../SpecialConstructorReference.java | 2 +-
.../key/java/reference/SuperReference.java | 2 +-
.../key/java/reference/ThisReference.java | 2 +-
.../key/java/reference/TypeReferenceImp.java | 2 +-
.../key/java/reference/VariableReference.java | 2 +-
.../uka/ilkd/key/java/statement/Assert.java | 2 +-
.../de/uka/ilkd/key/java/statement/Case.java | 2 +-
.../de/uka/ilkd/key/java/statement/Catch.java | 2 +-
.../key/java/statement/CatchAllStatement.java | 2 +-
.../uka/ilkd/key/java/statement/Ccatch.java | 2 +-
.../uka/ilkd/key/java/statement/Default.java | 2 +-
.../de/uka/ilkd/key/java/statement/Else.java | 2 +-
.../de/uka/ilkd/key/java/statement/Exec.java | 4 +-
.../statement/ExpressionJumpStatement.java | 2 +-
.../uka/ilkd/key/java/statement/Finally.java | 2 +-
.../ilkd/key/java/statement/ForUpdates.java | 2 +-
.../de/uka/ilkd/key/java/statement/Guard.java | 2 +-
.../de/uka/ilkd/key/java/statement/If.java | 4 +-
.../ilkd/key/java/statement/JmlAssert.java | 2 +-
.../java/statement/LabelJumpStatement.java | 2 +-
.../key/java/statement/LabeledStatement.java | 2 +-
.../uka/ilkd/key/java/statement/LoopInit.java | 2 +-
.../key/java/statement/LoopScopeBlock.java | 4 +-
.../key/java/statement/LoopStatement.java | 2 +-
.../java/statement/MergePointStatement.java | 2 +-
.../java/statement/MethodBodyStatement.java | 2 +-
.../ilkd/key/java/statement/MethodFrame.java | 8 ++--
.../ilkd/key/java/statement/SetStatement.java | 2 +-
.../uka/ilkd/key/java/statement/Switch.java | 2 +-
.../key/java/statement/SynchronizedBlock.java | 4 +-
.../de/uka/ilkd/key/java/statement/Then.java | 2 +-
.../java/statement/TransactionStatement.java | 2 +-
.../de/uka/ilkd/key/java/statement/Try.java | 4 +-
.../key/java/visitor/CreatingASTVisitor.java | 6 +--
.../key/java/visitor/FreeLabelFinder.java | 2 +-
.../InnerBreakAndContinueReplacer.java | 4 +-
.../ilkd/key/java/visitor/JavaASTWalker.java | 2 +-
.../OuterBreakContinueAndReturnReplacer.java | 4 +-
.../key/java/visitor/ProgramContextAdder.java | 6 +--
.../java/de/uka/ilkd/key/logic/JavaBlock.java | 17 +++++++-
.../ilkd/key/logic/op/ElementaryUpdate.java | 13 ++++++
.../de/uka/ilkd/key/logic/op/Equality.java | 11 +++++
.../uka/ilkd/key/logic/op/IfExThenElse.java | 11 +++++
.../de/uka/ilkd/key/logic/op/IfThenElse.java | 11 +++++
.../de/uka/ilkd/key/logic/op/Junctor.java | 11 +++++
.../uka/ilkd/key/logic/op/LogicVariable.java | 11 +++++
.../ilkd/key/logic/op/ObserverFunction.java | 18 ++++++--
.../uka/ilkd/key/logic/op/ProgramMethod.java | 2 +-
.../de/uka/ilkd/key/logic/op/ProgramSV.java | 2 +-
.../ilkd/key/logic/op/ProgramVariable.java | 12 ++++++
.../de/uka/ilkd/key/logic/op/Qualifier.java | 41 +++++++++++++++++++
.../de/uka/ilkd/key/logic/op/Quantifier.java | 11 +++++
.../key/logic/op/SortDependingFunction.java | 21 ++++++++--
.../de/uka/ilkd/key/logic/op/SubstOp.java | 12 ++++++
.../de/uka/ilkd/key/logic/op/TermLabelSV.java | 2 +-
.../ilkd/key/logic/op/UpdateApplication.java | 11 +++++
.../uka/ilkd/key/logic/op/UpdateJunctor.java | 11 +++++
.../ilkd/key/logic/sort/ProgramSVSort.java | 2 +-
.../de/uka/ilkd/key/pp/PrettyPrinter.java | 2 +-
.../de/uka/ilkd/key/proof/TacletIndex.java | 2 +-
.../key/rule/LoopInvariantBuiltInRuleApp.java | 2 +-
.../rule/conditions/StoreStmtInCondition.java | 2 +-
.../metaconstruct/ProgramTransformer.java | 2 +-
.../WhileLoopTransformation.java | 4 +-
.../key/speclang/jml/JMLSpecExtractor.java | 2 +-
.../key/java/TestContextStatementBlock.java | 2 +-
.../org/key_project/logic/SyntaxElement.java | 3 +-
.../logic/SyntaxElementCursor.java | 16 +++++---
.../main/java/org/key_project/logic/Term.java | 19 +++++++++
.../org/key_project/logic/op/Function.java | 11 +++++
.../org/key_project/logic/op/Modality.java | 28 ++++++++++++-
.../org/key_project/logic/op/Operator.java | 3 +-
.../ilkd/key/gui/sourceview/SourceView.java | 2 +-
129 files changed, 455 insertions(+), 150 deletions(-)
create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java
index 706723eaeab..07bee533ecd 100644
--- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java
+++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java
@@ -59,7 +59,7 @@ public LinkedHashSet> computeReferences(Node node, Services s
ExecutionContext context = extractContext(node, services);
LinkedHashSet> result =
new LinkedHashSet<>();
- for (int i = 0; i < assignment.getChildCount(); i++) {
+ for (int i = 0; i < assignment.getSyntaxChildCount(); i++) {
ProgramElement child = assignment.getChildAt(i);
if (child instanceof MethodReference) {
IProofReference reference =
diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java
index e37beeaa55b..49c35b4f0e6 100644
--- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java
+++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java
@@ -82,7 +82,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
ProofReferenceUtil.merge(toFill, reference);
}
} else if (includeExpressionContainer && pe instanceof ExpressionContainer ec) {
- for (int i = ec.getChildCount() - 1; i >= 0; i--) {
+ for (int i = ec.getSyntaxChildCount() - 1; i >= 0; i--) {
ProgramElement element = ec.getChildAt(i);
listReferences(node, element, arrayLength, toFill, includeExpressionContainer);
}
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java
index bfb10ac3e91..20a6a6e091e 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java
+++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java
@@ -120,7 +120,7 @@ protected void updateRelevantLocations(final ProgramElement read,
Location normalizedElement = normalizeAlias(services, relevantElement, info);
relevantLocations.add(normalizedElement);
} else if (read instanceof NonTerminalProgramElement ntpe) {
- for (int i = 0; i < ntpe.getChildCount(); i++) {
+ for (int i = 0; i < ntpe.getSyntaxChildCount(); i++) {
updateRelevantLocations(ntpe.getChildAt(i), relevantLocations, info, services);
}
}
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractSlicer.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractSlicer.java
index 56ead50dddb..3aab95bc564 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractSlicer.java
+++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractSlicer.java
@@ -792,7 +792,7 @@ protected Location computeRepresentativeAlias(Location location,
*/
protected ReferencePrefix toReferencePrefix(SourceElement sourceElement) {
if (sourceElement instanceof PassiveExpression) {
- if (((PassiveExpression) sourceElement).getChildCount() != 1) {
+ if (((PassiveExpression) sourceElement).getSyntaxChildCount() != 1) {
throw new IllegalStateException(
"PassiveExpression '" + sourceElement + "' has not exactly one child.");
}
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/ExceptionBreakpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/ExceptionBreakpoint.java
index bb81a7f3e64..74c23775aff 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/ExceptionBreakpoint.java
+++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/ExceptionBreakpoint.java
@@ -104,7 +104,7 @@ public boolean isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, P
Node node) {
Node SETParent = SymbolicExecutionUtil.findParentSetNode(node);
if (activeStatement instanceof Throw throwStatement && isEnabled()) {
- for (int i = 0; i < throwStatement.getChildCount(); i++) {
+ for (int i = 0; i < throwStatement.getSyntaxChildCount(); i++) {
SourceElement childElement = throwStatement.getChildAt(i);
if (childElement instanceof LocationVariable locVar) {
if (locVar.getKeYJavaType().getSort().toString().equals(exceptionName)
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/FieldWatchpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/FieldWatchpoint.java
index d1082bca4c9..a3246cc6949 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/FieldWatchpoint.java
+++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/FieldWatchpoint.java
@@ -80,7 +80,7 @@ public boolean isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, P
private boolean checkChildrenOfSourceElement(SourceElement sourceElement) {
boolean found = false;
if (sourceElement instanceof Assignment assignment) {
- for (int i = 1; i < assignment.getChildCount(); i++) {
+ for (int i = 1; i < assignment.getSyntaxChildCount(); i++) {
SourceElement childElement = assignment.getChildAt(i);
if (childElement instanceof FieldReference field && ((FieldReference) childElement)
.getProgramVariable().name().toString().equals(fullFieldName)) {
@@ -93,7 +93,7 @@ private boolean checkChildrenOfSourceElement(SourceElement sourceElement) {
}
}
} else if (sourceElement instanceof NonTerminalProgramElement programElement) {
- for (int i = 0; i < programElement.getChildCount(); i++) {
+ for (int i = 0; i < programElement.getSyntaxChildCount(); i++) {
SourceElement childElement = programElement.getChildAt(i);
if (childElement instanceof FieldReference field && ((FieldReference) childElement)
.getProgramVariable().name().toString().equals(fullFieldName)) {
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/SymbolicExecutionExceptionBreakpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/SymbolicExecutionExceptionBreakpoint.java
index 18787225830..995917eef20 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/SymbolicExecutionExceptionBreakpoint.java
+++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/SymbolicExecutionExceptionBreakpoint.java
@@ -93,7 +93,7 @@ public void updateState(int maxApplications, long timeout, Proof proof, long sta
SourceElement activeStatement = NodeInfo.computeActiveStatement(ruleApp);
Node SETParent = SymbolicExecutionUtil.findParentSetNode(node);
if (activeStatement instanceof Throw throwStatement && isEnabled()) {
- for (int i = 0; i < throwStatement.getChildCount(); i++) {
+ for (int i = 0; i < throwStatement.getSyntaxChildCount(); i++) {
SourceElement childElement = throwStatement.getChildAt(i);
if (childElement instanceof LocationVariable locVar) {
if (locVar.getKeYJavaType().getSort().toString().equals(exceptionName)
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java
index 785b03e3d80..fa13eb0fe87 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java
+++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java
@@ -3951,10 +3951,10 @@ public static Pair computeSecondStatement(RuleApp ruleAp
}
// Compute second statement
StatementBlock block = null;
- while (!blocks.isEmpty() && (block == null || block.getChildCount() < 2)) {
+ while (!blocks.isEmpty() && (block == null || block.getSyntaxChildCount() < 2)) {
block = blocks.removeFirst();
}
- if (block != null && block.getChildCount() >= 2) {
+ if (block != null && block.getSyntaxChildCount() >= 2) {
return new Pair<>(methodFrameCount, block.getChildAt(1));
} else {
return new Pair<>(methodFrameCount, null);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakLabelParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakLabelParameterDeclaration.java
index 792cf39949a..f072563e45c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakLabelParameterDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakLabelParameterDeclaration.java
@@ -21,7 +21,7 @@ public CcatchBreakLabelParameterDeclaration(ExtList children) {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (label != null) ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakParameterDeclaration.java
index 8bd2af73e20..05bb1d123f7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakParameterDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakParameterDeclaration.java
@@ -18,7 +18,7 @@ public CcatchBreakParameterDeclaration(ExtList children) {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakWildcardParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakWildcardParameterDeclaration.java
index 51938d23965..69b416cef06 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakWildcardParameterDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchBreakWildcardParameterDeclaration.java
@@ -18,7 +18,7 @@ public CcatchBreakWildcardParameterDeclaration(ExtList children) {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueLabelParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueLabelParameterDeclaration.java
index 1c5544866f6..a16bf704d2d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueLabelParameterDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueLabelParameterDeclaration.java
@@ -21,7 +21,7 @@ public CcatchContinueLabelParameterDeclaration(ExtList children) {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (label != null) ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueParameterDeclaration.java
index e01e4739c8b..47f2a481df7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueParameterDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueParameterDeclaration.java
@@ -18,7 +18,7 @@ public CcatchContinueParameterDeclaration(ExtList children) {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueWildcardParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueWildcardParameterDeclaration.java
index 984ab585973..bad98ad62f4 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueWildcardParameterDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchContinueWildcardParameterDeclaration.java
@@ -19,7 +19,7 @@ public CcatchContinueWildcardParameterDeclaration(ExtList children) {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchReturnParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchReturnParameterDeclaration.java
index 838ca7e192a..6345841c16a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchReturnParameterDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchReturnParameterDeclaration.java
@@ -18,7 +18,7 @@ public CcatchReturnParameterDeclaration(ExtList children) {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchReturnValParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchReturnValParameterDeclaration.java
index 88aaee039ce..78a8bdd40b0 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/CcatchReturnValParameterDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/CcatchReturnValParameterDeclaration.java
@@ -43,7 +43,7 @@ public ImmutableArray getVariables() {
* @return an int giving the number of children of this node
*/
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return delegate != null ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java b/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java
index 0d556acb369..33b0d882c62 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java
@@ -5,6 +5,8 @@
import de.uka.ilkd.key.java.visitor.Visitor;
+import org.key_project.logic.SyntaxElement;
+
/**
* Comment element of Java source code.
*/
@@ -71,4 +73,14 @@ public boolean equals(Object o) {
}
return (getText().equals(cmp.getText()));
}
+
+ @Override
+ public int getSyntaxChildCount() {
+ return 0;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException("Comment has no children");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java b/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java
index 1f4573e5f3f..c8540345aff 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java
@@ -72,12 +72,12 @@ public CompilationUnit(ExtList children) {
public SourceElement getFirstElement() {
- return (getChildCount() > 0) ? getChildAt(0).getFirstElement() : this;
+ return (getSyntaxChildCount() > 0) ? getChildAt(0).getFirstElement() : this;
}
@Override
public SourceElement getFirstElementIncludingBlocks() {
- return (getChildCount() > 0) ? getChildAt(0).getFirstElementIncludingBlocks() : this;
+ return (getSyntaxChildCount() > 0) ? getChildAt(0).getFirstElementIncludingBlocks() : this;
}
public SourceElement getLastElement() {
@@ -101,7 +101,7 @@ public String getName() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (packageSpec != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java
index 408d81bbdb1..b8deb7f0d83 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java
@@ -88,12 +88,12 @@ public IExecutionContext getExecutionContext() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int count = 0;
if (executionContext != null) {
count++;
}
- count += super.getChildCount();
+ count += super.getSyntaxChildCount();
return count;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Import.java b/key.core/src/main/java/de/uka/ilkd/key/java/Import.java
index 500d659b836..43bd217e901 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/Import.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/Import.java
@@ -88,7 +88,7 @@ public boolean isMultiImport() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (reference != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java
index ded5c975478..af7148c5398 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java
@@ -5,6 +5,7 @@
import de.uka.ilkd.key.rule.MatchConditions;
+import org.key_project.logic.SyntaxElement;
import org.key_project.util.ExtList;
import org.key_project.util.collection.ImmutableArray;
@@ -69,11 +70,11 @@ public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) {
}
final JavaNonTerminalProgramElement jnte = (JavaNonTerminalProgramElement) se;
- if (jnte.getChildCount() != getChildCount()) {
+ if (jnte.getSyntaxChildCount() != getSyntaxChildCount()) {
return false;
}
- for (int i = 0, cc = getChildCount(); i < cc; i++) {
+ for (int i = 0, cc = getSyntaxChildCount(); i < cc; i++) {
if (!getChildAt(i).equalsModRenaming(jnte.getChildAt(i), nat)) {
return false;
}
@@ -89,7 +90,7 @@ public boolean equals(Object o) {
@Override
protected int computeHashCode() {
int localHash = 17 * super.computeHashCode();
- for (int i = 0, sz = getChildCount(); i < sz; i++) {
+ for (int i = 0, sz = getSyntaxChildCount(); i < sz; i++) {
final ProgramElement pe = getChildAt(i);
localHash = 17 * localHash + (pe == null ? 0 : pe.hashCode());
}
@@ -148,7 +149,7 @@ protected boolean compatibleBlockSize(int pos, int max) {
protected MatchConditions matchChildren(SourceData source, MatchConditions matchCond,
int offset) {
- for (int i = offset, sz = getChildCount(); i < sz; i++) {
+ for (int i = offset, sz = getSyntaxChildCount(); i < sz; i++) {
matchCond = getChildAt(i).match(source, matchCond);
if (matchCond == null) {
return null;
@@ -157,10 +158,15 @@ protected MatchConditions matchChildren(SourceData source, MatchConditions match
final NonTerminalProgramElement ntSrc = (NonTerminalProgramElement) source.getElement();
- if (!compatibleBlockSize(source.getChildPos(), ntSrc.getChildCount())) {
+ if (!compatibleBlockSize(source.getChildPos(), ntSrc.getSyntaxChildCount())) {
return null;
}
return matchCond;
}
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ return getChildAt(n);
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java
index ca20a719d4d..97368ebdad2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java
@@ -14,7 +14,7 @@ public interface NonTerminalProgramElement extends ProgramElement {
*
* @return an int giving the number of children of this node
*/
- int getChildCount();
+ int getSyntaxChildCount();
/**
* Returns the child at the specified index in this node's "virtual" child array.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/PackageSpecification.java b/key.core/src/main/java/de/uka/ilkd/key/java/PackageSpecification.java
index 1adeb3a75d5..82a9d5de4fb 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/PackageSpecification.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/PackageSpecification.java
@@ -46,7 +46,7 @@ public SourceElement getLastElement() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (reference != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SourceData.java b/key.core/src/main/java/de/uka/ilkd/key/java/SourceData.java
index 0c34b1c15bf..e56178bde54 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/SourceData.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/SourceData.java
@@ -99,7 +99,7 @@ public ProgramElement getSource() {
final NonTerminalProgramElement ntpe = (NonTerminalProgramElement) element;
- if (childPos < ntpe.getChildCount()) {
+ if (childPos < ntpe.getSyntaxChildCount()) {
return ntpe.getChildAt(childPos);
} else {
return null;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java
index 046d51538cb..d9709324c9d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java
@@ -6,13 +6,15 @@
import de.uka.ilkd.key.java.visitor.Visitor;
import de.uka.ilkd.key.logic.op.SVSubstitute;
+import org.key_project.logic.SyntaxElement;
+
/**
* A source element is a piece of syntax. It does not necessarily have a semantics, at least none
* that is machinable, for instance a {@link recoder.java.Comment}. taken from RECODER and changed
* to achieve an immutable structure
*/
-public interface SourceElement extends SVSubstitute {
+public interface SourceElement extends SVSubstitute, SyntaxElement {
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java
index 6d0c95695c8..0fe7c811033 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java
@@ -121,7 +121,7 @@ public final boolean isEmpty() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return body.size();
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java
index 902e791ace6..b0cc3d15ece 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java
@@ -3,9 +3,20 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.java;
+import org.key_project.logic.SyntaxElement;
+
/**
* Terminal program element. taken from COMPOST and changed to achieve an immutable structure
*/
public interface TerminalProgramElement extends ProgramElement {
+ @Override
+ default int getSyntaxChildCount() {
+ return 0;
+ }
+
+ @Override
+ default SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException("Program element " + this + " has no children");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ArrayDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ArrayDeclaration.java
index c432502f14d..a689408a21a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ArrayDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ArrayDeclaration.java
@@ -71,7 +71,7 @@ public ArrayDeclaration(ExtList children, TypeReference baseType, KeYJavaType su
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (modArray != null) {
result += modArray.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ClassDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ClassDeclaration.java
index 269dc7f999a..a9ab43f9e41 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ClassDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ClassDeclaration.java
@@ -117,7 +117,7 @@ public ClassDeclaration(ExtList children, ProgramElementName fullName, boolean i
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (modArray != null) {
result += modArray.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ClassInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ClassInitializer.java
index aebf56f774e..2a35ae21d8f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ClassInitializer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ClassInitializer.java
@@ -70,7 +70,7 @@ public Statement getStatementAt(int index) {
}
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (modArray != null) {
result += modArray.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/FieldDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/FieldDeclaration.java
index 26223d4712b..b3dbd242dd7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/FieldDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/FieldDeclaration.java
@@ -66,7 +66,7 @@ public ImmutableArray extends VariableSpecification> getVariables() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (modArray != null) {
result += modArray.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/InheritanceSpecification.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/InheritanceSpecification.java
index df4cebda29f..631c6aecb4d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/InheritanceSpecification.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/InheritanceSpecification.java
@@ -82,7 +82,7 @@ public SourceElement getLastElement() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (supertypes != null) {
result += supertypes.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/InterfaceDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/InterfaceDeclaration.java
index 201ab2f32ea..baf29255751 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/InterfaceDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/InterfaceDeclaration.java
@@ -65,7 +65,7 @@ public InterfaceDeclaration(ProgramElementName name) {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (modArray != null) {
result += modArray.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/LocalVariableDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/LocalVariableDeclaration.java
index 710ed417aa5..16a18b6a58c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/LocalVariableDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/LocalVariableDeclaration.java
@@ -121,7 +121,7 @@ public ImmutableArray getVariables() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (modArray != null) {
result += modArray.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java
index 04346acf3a7..04a1aa6cf0b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java
@@ -163,12 +163,12 @@ public SourceElement getFirstElement() {
@Override
public SourceElement getLastElement() {
- return getChildAt(getChildCount() - 1).getLastElement();
+ return getChildAt(getSyntaxChildCount() - 1).getLastElement();
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (modArray != null) {
result += modArray.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ParameterDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ParameterDeclaration.java
index 75c08a72be7..75685e606d5 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ParameterDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ParameterDeclaration.java
@@ -109,7 +109,7 @@ public ImmutableArray getVariables() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (modArray != null) {
result += modArray.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/SuperArrayDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/SuperArrayDeclaration.java
index 67f52df42bc..55cd9a967b3 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/SuperArrayDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/SuperArrayDeclaration.java
@@ -28,7 +28,7 @@ public SuperArrayDeclaration(FieldDeclaration length) {
this(new ProgramElementName("SuperArray"), length);
}
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Throws.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Throws.java
index 35d0279ec88..80eb623695c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Throws.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Throws.java
@@ -77,7 +77,7 @@ public SourceElement getLastElement() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (exceptions != null) {
result += exceptions.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableDeclaration.java
index 185194af413..a6124472682 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableDeclaration.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableDeclaration.java
@@ -95,7 +95,7 @@ public SourceElement getFirstElementIncludingBlocks() {
}
public SourceElement getLastElement() {
- return getChildAt(getChildCount() - 1).getLastElement();
+ return getChildAt(getSyntaxChildCount() - 1).getLastElement();
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableSpecification.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableSpecification.java
index 787cf6b874e..6c28e9a0ad8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableSpecification.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableSpecification.java
@@ -100,7 +100,7 @@ public VariableSpecification(ExtList children, IProgramVariable var, int dim, Ty
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (var != null) {
result++;
@@ -280,10 +280,10 @@ public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) {
}
}
nat.add(var, vs.getProgramVariable());
- if (vs.getChildCount() != getChildCount()) {
+ if (vs.getSyntaxChildCount() != getSyntaxChildCount()) {
return false;
}
- for (int i = 0, cc = getChildCount(); i < cc; i++) {
+ for (int i = 0, cc = getSyntaxChildCount(); i < cc; i++) {
if (!getChildAt(i).equalsModRenaming(vs.getChildAt(i), nat)) {
return false;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/AnnotationUseSpecification.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/AnnotationUseSpecification.java
index fa81c6b4a6d..18266529523 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/AnnotationUseSpecification.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/AnnotationUseSpecification.java
@@ -39,7 +39,7 @@ public ProgramElement getChildAt(int index) {
throw new ArrayIndexOutOfBoundsException();
}
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 1;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/ArrayInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/ArrayInitializer.java
index 5e1a0fe937b..a4f9abffeb8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/ArrayInitializer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/ArrayInitializer.java
@@ -54,7 +54,7 @@ public ArrayInitializer(Expression[] expressions, KeYJavaType kjt) {
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (children != null) ? children.size() : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java
index ff1a653287a..952f7e1b5da 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java
@@ -143,7 +143,7 @@ public SourceElement getLastElement() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (children != null) ? children.size() : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/ExactInstanceof.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/ExactInstanceof.java
index a76c65a7676..f327fa68264 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/ExactInstanceof.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/ExactInstanceof.java
@@ -43,7 +43,7 @@ public ExactInstanceof(Expression unaryChild, TypeReference typeref) {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (children != null) {
result += children.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java
index 284c254db72..a3ba9852625 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java
@@ -31,13 +31,13 @@ public class Instanceof extends TypeOperator {
public Instanceof(ExtList children) {
super(children);
- assert getChildCount() == 2 : "not 2 children but " + getChildCount();
+ assert this.getSyntaxChildCount() == 2 : "not 2 children but " + this.getSyntaxChildCount();
}
public Instanceof(Expression unaryChild, TypeReference typeref) {
super(unaryChild, typeref);
- assert getChildCount() == 2 : "not 2 children but " + getChildCount();
+ assert this.getSyntaxChildCount() == 2 : "not 2 children but " + this.getSyntaxChildCount();
}
/**
@@ -46,7 +46,7 @@ public Instanceof(Expression unaryChild, TypeReference typeref) {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (children != null) {
result += children.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/New.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/New.java
index bc7027d5498..51062cc9558 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/New.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/New.java
@@ -99,7 +99,7 @@ public SourceElement getFirstElementIncludingBlocks() {
@Override
public SourceElement getLastElement() {
- return getChildAt(getChildCount() - 1).getLastElement();
+ return getChildAt(this.getSyntaxChildCount() - 1).getLastElement();
}
@@ -142,7 +142,7 @@ public TypeDeclaration getTypeDeclarationAt(int index) {
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (accessPath != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/NewArray.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/NewArray.java
index 2496a1a84cd..e88712ff847 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/NewArray.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/NewArray.java
@@ -148,7 +148,7 @@ public ArrayInitializer getArrayInitializer() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (typeReference != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/TypeCast.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/TypeCast.java
index 76ac7b3c5a1..f6b3d467215 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/TypeCast.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/TypeCast.java
@@ -49,7 +49,7 @@ public TypeCast(ExtList children) {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (typeReference != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/ArrayLengthReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/ArrayLengthReference.java
index c12d07be94d..d141a83bd81 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/ArrayLengthReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/ArrayLengthReference.java
@@ -49,7 +49,7 @@ public ArrayLengthReference(ExtList children) {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (prefix != null) ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/ArrayReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/ArrayReference.java
index 667f011688b..abba0a21f91 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/ArrayReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/ArrayReference.java
@@ -184,7 +184,7 @@ public ReferencePrefix getReferencePrefix() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (prefix != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/ExecutionContext.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/ExecutionContext.java
index c9a1ba78a12..3c0aab03cd8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/ExecutionContext.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/ExecutionContext.java
@@ -63,7 +63,7 @@ public ExecutionContext(ExtList children) {
* @return an int giving the number of children of this node
*/
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int count = 0;
if (classContext != null) {
count++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java
index 0616f1b3c7e..e6d3b6f61af 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java
@@ -56,7 +56,7 @@ public FieldReference(ProgramVariable pv, ReferencePrefix prefix, PositionInfo p
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (prefix != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/MetaClassReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/MetaClassReference.java
index 446d332ff55..2305cf42a18 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/MetaClassReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/MetaClassReference.java
@@ -54,7 +54,7 @@ public MetaClassReference(ExtList children) {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (typeReference != null) ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/MethodReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/MethodReference.java
index e31c8e827b3..7b48aaaab09 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/MethodReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/MethodReference.java
@@ -117,7 +117,7 @@ public ReferencePrefix getReferencePrefix() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (prefix != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/PackageReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/PackageReference.java
index fdccddd95cc..fc821d1c24d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/PackageReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/PackageReference.java
@@ -63,7 +63,7 @@ public SourceElement getFirstElementIncludingBlocks() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (prefix != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java
index 97c27ac7abc..130c07b1c93 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java
@@ -43,7 +43,7 @@ public SchematicFieldReference(ExtList children, ReferencePrefix prefix) {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (prefix != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/SpecialConstructorReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/SpecialConstructorReference.java
index bb05f76b56c..81e6e2baf4b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/SpecialConstructorReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/SpecialConstructorReference.java
@@ -77,7 +77,7 @@ public SpecialConstructorReference(ExtList children, PositionInfo pi) {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return getExpressionCount();
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/SuperReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/SuperReference.java
index ad5d2828d63..11d9725c4a7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/SuperReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/SuperReference.java
@@ -73,7 +73,7 @@ public ReferencePrefix getReferencePrefix() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int count = 0;
if (prefix != null) {
count++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/ThisReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/ThisReference.java
index 6c04bf116a3..573444a7bff 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/ThisReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/ThisReference.java
@@ -66,7 +66,7 @@ public SourceElement getFirstElementIncludingBlocks() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int count = 0;
if (prefix != null) {
count++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/TypeReferenceImp.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/TypeReferenceImp.java
index f70a47f3e46..a05c177b7ec 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/TypeReferenceImp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/TypeReferenceImp.java
@@ -80,7 +80,7 @@ public SourceElement getFirstElementIncludingBlocks() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (prefix != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/VariableReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/VariableReference.java
index 8b2d4a86702..6d127891693 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/VariableReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/VariableReference.java
@@ -41,7 +41,7 @@ public ProgramElementName getProgramElementName() {
return (ProgramElementName) variable.name();
}
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (variable != null) ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Assert.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Assert.java
index 1cffa3aa4e6..065e882b968 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Assert.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Assert.java
@@ -41,7 +41,7 @@ public ProgramElement getChildAt(int index) {
return getExpressionAt(index);
}
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return getExpressionCount();
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java
index c1c9535b626..6b24a389b40 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java
@@ -76,7 +76,7 @@ public Case(ExtList children, Expression expr, PositionInfo pos) {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (expression != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Catch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Catch.java
index 4ab7438bc60..bf1d64d22c7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Catch.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Catch.java
@@ -70,7 +70,7 @@ public SourceElement getLastElement() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (parameter != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/CatchAllStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/CatchAllStatement.java
index bb7690aa055..b0387cb822f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/CatchAllStatement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/CatchAllStatement.java
@@ -44,7 +44,7 @@ public LocationVariable getParam() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int i = 0;
if (body != null) {
i++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Ccatch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Ccatch.java
index e3126a5ebe6..3e8558efbf8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Ccatch.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Ccatch.java
@@ -99,7 +99,7 @@ public boolean hasNonStdParameterDeclaration() {
* @return an int giving the number of children of this node
*/
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (hasParameterDeclaration()) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java
index 6536464ed76..d1d4960d423 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java
@@ -54,7 +54,7 @@ public Default(ExtList children) {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (body != null) {
result += body.size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Else.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Else.java
index 63dc0c92e63..154fffc633e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Else.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Else.java
@@ -54,7 +54,7 @@ public SourceElement getLastElement() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (body != null) ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java
index 32774cb8f19..5afad68e81b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java
@@ -131,7 +131,7 @@ public SourceElement getFirstElement() {
@Override
public SourceElement getLastElement() {
- return getChildAt(getChildCount() - 1).getLastElement();
+ return getChildAt(getSyntaxChildCount() - 1).getLastElement();
}
/**
@@ -140,7 +140,7 @@ public SourceElement getLastElement() {
* @return an int giving the number of children of this node
*/
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (body != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ExpressionJumpStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ExpressionJumpStatement.java
index 4bddeab80a7..2a1d810627d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ExpressionJumpStatement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ExpressionJumpStatement.java
@@ -85,7 +85,7 @@ public Expression getExpression() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (expression != null) ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Finally.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Finally.java
index bd4e40b6d8b..24c2db9ea17 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Finally.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Finally.java
@@ -52,7 +52,7 @@ public Finally(ExtList children) {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (body != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ForUpdates.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ForUpdates.java
index 3823a2ab3be..3626fccfc96 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ForUpdates.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ForUpdates.java
@@ -69,7 +69,7 @@ public void visit(Visitor v) {
v.performActionOnForUpdates(this);
}
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return getExpressionCount();
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Guard.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Guard.java
index d1483fed22a..70c883985bd 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Guard.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Guard.java
@@ -33,7 +33,7 @@ public void visit(Visitor v) {
v.performActionOnGuard(this);
}
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (expr != null) ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/If.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/If.java
index e9f451dc038..25a8be2825c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/If.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/If.java
@@ -88,7 +88,7 @@ public If(Expression e, Then thenBranch, Else elseBranch) {
* @return
*/
public SourceElement getLastElement() {
- return getChildAt(getChildCount() - 1).getLastElement();
+ return getChildAt(getSyntaxChildCount() - 1).getLastElement();
}
/**
@@ -97,7 +97,7 @@ public SourceElement getLastElement() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
if (elseBranch != null) {
return 3;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/JmlAssert.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/JmlAssert.java
index 732174aa2fd..8254ebcbe92 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/JmlAssert.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/JmlAssert.java
@@ -149,7 +149,7 @@ protected int computeHashCode() {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabelJumpStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabelJumpStatement.java
index 68d1c45a7b2..755e228811a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabelJumpStatement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabelJumpStatement.java
@@ -93,7 +93,7 @@ public ProgramElementName getProgramElementName() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (name != null) ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java
index 7a8fffc97ca..6ac702ba7be 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java
@@ -211,7 +211,7 @@ public Statement getBody() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (name != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopInit.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopInit.java
index f3f6e918d8c..289ab69dd81 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopInit.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopInit.java
@@ -74,7 +74,7 @@ public void visit(Visitor v) {
v.performActionOnLoopInit(this);
}
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return getStatementCount();
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java
index 90b373e1438..edd36bc8d50 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java
@@ -107,7 +107,7 @@ public ImmutableArray getPrefixElements() {
@Override
public PosInProgram getFirstActiveChildPos() {
return getStatementCount() == 0 ? PosInProgram.TOP
- : PosInProgram.TOP.down(getChildCount() - 1).down(0);
+ : PosInProgram.TOP.down(this.getSyntaxChildCount() - 1).down(0);
}
/**
@@ -150,7 +150,7 @@ public IProgramVariable getIndexPV() {
* @return an int giving the number of children of this node
*/
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (indexPV != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopStatement.java
index af0b8c08b57..d2f68f3de43 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopStatement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopStatement.java
@@ -217,7 +217,7 @@ static private ExtList add(ExtList e, Object o) {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (inits != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MergePointStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/MergePointStatement.java
index 1749900d64d..0de156b2627 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MergePointStatement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/MergePointStatement.java
@@ -82,7 +82,7 @@ public Expression getExpression() {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (identifier != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodBodyStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodBodyStatement.java
index 60d8aa4206b..33be238c465 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodBodyStatement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodBodyStatement.java
@@ -161,7 +161,7 @@ public Statement getBody(Services services) {
*
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int i = 0;
if (bodySource != null) {
i++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java
index ede5682ff23..224239aaa71 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java
@@ -53,7 +53,8 @@ public MethodFrame(IProgramVariable resultVar, IExecutionContext execContext,
this.execContext = execContext;
firstActiveChildPos =
- body.isEmpty() ? PosInProgram.TOP : PosInProgram.TOP.down(getChildCount() - 1).down(0);
+ body.isEmpty() ? PosInProgram.TOP
+ : PosInProgram.TOP.down(getSyntaxChildCount() - 1).down(0);
Debug.assertTrue(execContext != null, "methodframe: executioncontext missing");
Debug.assertTrue(body != null, "methodframe: body missing");
@@ -78,7 +79,8 @@ public MethodFrame(IProgramVariable resultVar, IExecutionContext execContext,
this.execContext = execContext;
firstActiveChildPos =
- body.isEmpty() ? PosInProgram.TOP : PosInProgram.TOP.down(getChildCount() - 1).down(0);
+ body.isEmpty() ? PosInProgram.TOP
+ : PosInProgram.TOP.down(getSyntaxChildCount() - 1).down(0);
Debug.assertTrue(execContext != null, "methodframe: executioncontext missing");
@@ -185,7 +187,7 @@ public IProgramMethod getProgramMethod() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (resultVar != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SetStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SetStatement.java
index 0ece40806f5..5bbdd77569e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SetStatement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SetStatement.java
@@ -62,7 +62,7 @@ public void visit(Visitor v) {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java
index 3816e6f9282..f4a2b7ca6eb 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java
@@ -81,7 +81,7 @@ public Switch(ExtList children) {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (expression != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java
index 492cfc5b683..d0bc46c3c61 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java
@@ -135,7 +135,7 @@ private boolean expressionWithoutSideffects() {
public PosInProgram getFirstActiveChildPos() {
return getStatementCount() == 0 ? PosInProgram.TOP
: (expressionWithoutSideffects()
- ? PosInProgram.TOP.down(getChildCount() - 1).down(0)
+ ? PosInProgram.TOP.down(getSyntaxChildCount() - 1).down(0)
: PosInProgram.ONE);
}
@@ -183,7 +183,7 @@ public Expression getExpression() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (expression != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Then.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Then.java
index a87fd000787..37ed703cd92 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Then.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Then.java
@@ -65,7 +65,7 @@ public SourceElement getLastElement() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return (body != null) ? 1 : 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/TransactionStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/TransactionStatement.java
index 00c17a5e034..6ae42412b2a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/TransactionStatement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/TransactionStatement.java
@@ -39,7 +39,7 @@ public ProgramElement getChildAt(int index) {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java
index 9011234e233..01c2c35e49a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java
@@ -137,7 +137,7 @@ public SourceElement getFirstElement() {
public SourceElement getLastElement() {
- return getChildAt(getChildCount() - 1).getLastElement();
+ return getChildAt(this.getSyntaxChildCount() - 1).getLastElement();
}
/**
@@ -146,7 +146,7 @@ public SourceElement getLastElement() {
* @return an int giving the number of children of this node
*/
- public int getChildCount() {
+ public int getSyntaxChildCount() {
int result = 0;
if (body != null) {
result++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java
index 31bb841ed14..b8cdb2acdeb 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java
@@ -543,11 +543,11 @@ public void performActionOnMethodFrame(MethodFrame x) {
pi = PositionInfo.UNDEFINED;
}
- if (x.getChildCount() == 3) {
+ if (x.getSyntaxChildCount() == 3) {
addChild(new MethodFrame((IProgramVariable) changeList.get(0),
(IExecutionContext) changeList.get(1), (StatementBlock) changeList.get(2), pi));
- } else if (x.getChildCount() == 2) {
+ } else if (x.getSyntaxChildCount() == 2) {
addChild(new MethodFrame(null, (IExecutionContext) changeList.get(0),
(StatementBlock) changeList.get(1), pi));
} else {
@@ -1527,7 +1527,7 @@ ProgramElement createNewElement(ExtList changeList) {
* @return pe2's position in pe1
*/
protected static int getPosition(NonTerminalProgramElement pe1, ProgramElement pe2) {
- int n = pe1.getChildCount();
+ int n = pe1.getSyntaxChildCount();
int i = 0;
while ((i < n) && (pe1.getChildAt(i) != pe2)) {
i++;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/FreeLabelFinder.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/FreeLabelFinder.java
index cd4968add8d..55e251fb36b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/FreeLabelFinder.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/FreeLabelFinder.java
@@ -20,7 +20,7 @@ public boolean findLabel(Label label, ProgramElement node) {
if (!(node instanceof LabeledStatement
&& ((LabeledStatement) node).getLabel().equals(label))) {
if (node instanceof NonTerminalProgramElement nonTerminalNode) {
- for (int i = 0; i < nonTerminalNode.getChildCount(); i++) {
+ for (int i = 0; i < nonTerminalNode.getSyntaxChildCount(); i++) {
if (nonTerminalNode.getChildAt(i) != null) {
if (findLabel(label, nonTerminalNode.getChildAt(i))) {
return true;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/InnerBreakAndContinueReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/InnerBreakAndContinueReplacer.java
index bbb9fbfe280..35c3b1e4d1a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/InnerBreakAndContinueReplacer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/InnerBreakAndContinueReplacer.java
@@ -285,11 +285,11 @@ public void performActionOnMethodFrame(final MethodFrame x) {
final ExtList changeList = stack.peek();
if (!changeList.isEmpty() && changeList.getFirst() == CHANGED) {
changeList.removeFirst();
- if (x.getChildCount() == 3) {
+ if (x.getSyntaxChildCount() == 3) {
addChild(new MethodFrame((IProgramVariable) changeList.get(0),
(IExecutionContext) changeList.get(1), (StatementBlock) changeList.get(2),
PositionInfo.UNDEFINED));
- } else if (x.getChildCount() == 2) {
+ } else if (x.getSyntaxChildCount() == 2) {
addChild(new MethodFrame(null, (IExecutionContext) changeList.get(0),
(StatementBlock) changeList.get(1), PositionInfo.UNDEFINED));
} else {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTWalker.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTWalker.java
index 125f6dbdd5c..3dd9391d1fd 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTWalker.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTWalker.java
@@ -63,7 +63,7 @@ public int depth() {
protected void walk(ProgramElement node) {
if (node instanceof NonTerminalProgramElement nonTerminalNode) {
depth++;
- for (int i = 0; i < nonTerminalNode.getChildCount(); i++) {
+ for (int i = 0; i < nonTerminalNode.getSyntaxChildCount(); i++) {
if (nonTerminalNode.getChildAt(i) != null) {
walk(nonTerminalNode.getChildAt(i));
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java
index a796487d7d1..c6c560ffb4f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java
@@ -303,12 +303,12 @@ public void performActionOnMethodFrame(final MethodFrame x) {
final ExtList changeList = stack.peek();
if (!changeList.isEmpty() && changeList.getFirst() == CHANGED) {
changeList.removeFirst();
- if (x.getChildCount() == 3) {
+ if (x.getSyntaxChildCount() == 3) {
addChild(new MethodFrame((IProgramVariable) changeList.get(0),
(IExecutionContext) changeList.get(1), (StatementBlock) changeList.get(2),
PositionInfo.UNDEFINED));
- } else if (x.getChildCount() == 2) {
+ } else if (x.getSyntaxChildCount() == 2) {
addChild(new MethodFrame(null, (IExecutionContext) changeList.get(0),
(StatementBlock) changeList.get(1), PositionInfo.UNDEFINED));
} else {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java
index 589b1cb9d4d..49df58e0032 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java
@@ -110,12 +110,12 @@ protected JavaNonTerminalProgramElement wrap(JavaNonTerminalProgramElement conte
private final StatementBlock createWrapperBody(JavaNonTerminalProgramElement wrapper,
StatementBlock putIn, PosInProgram suffix) {
- final int putInLength = putIn.getChildCount();
+ final int putInLength = putIn.getSyntaxChildCount();
// ATTENTION: may be -1
final int lastChild = suffix.last();
- final int childLeft = wrapper.getChildCount() - lastChild;
+ final int childLeft = wrapper.getSyntaxChildCount() - lastChild;
final int childrenToAdd = putInLength + childLeft;
@@ -182,7 +182,7 @@ protected MethodFrame createMethodFrameWrapper(MethodFrame old, StatementBlock b
protected LabeledStatement createLabeledStatementWrapper(LabeledStatement old,
JavaNonTerminalProgramElement body) {
return new LabeledStatement(old.getLabel(),
- body instanceof StatementBlock && body.getChildCount() == 1
+ body instanceof StatementBlock && body.getSyntaxChildCount() == 1
&& !(body.getChildAt(0) instanceof LocalVariableDeclaration)
? (Statement) body.getChildAt(0)
: (Statement) body,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java b/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java
index b7d72e26382..2dd935eda54 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java
@@ -8,6 +8,7 @@
import de.uka.ilkd.key.pp.PrettyPrinter;
import org.key_project.logic.Program;
+import org.key_project.logic.SyntaxElement;
import org.key_project.util.EqualsModProofIrrelevancy;
import org.slf4j.Logger;
@@ -64,7 +65,7 @@ public boolean isEmpty() {
public int size() {
if ((program() instanceof StatementBlock)) {
- return ((StatementBlock) program()).getChildCount();
+ return ((StatementBlock) program()).getSyntaxChildCount();
}
return 0;
}
@@ -128,4 +129,18 @@ public int hashCodeModProofIrrelevancy() {
}
return hashCode;
}
+
+ @Override
+ public int getSyntaxChildCount() {
+ if (prg == null || this == EMPTY_JAVABLOCK)
+ return 0;
+ return 1;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ if (n == 0)
+ return prg;
+ throw new IndexOutOfBoundsException("JavaBlock " + this + " has only one child");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java
index 0837fda6089..9ae7934762d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java
@@ -9,6 +9,7 @@
import de.uka.ilkd.key.ldt.JavaDLTheory;
import org.key_project.logic.Name;
+import org.key_project.logic.SyntaxElement;
import org.key_project.logic.sort.Sort;
@@ -58,4 +59,16 @@ public static ElementaryUpdate getInstance(UpdateableOperator lhs) {
public UpdateableOperator lhs() {
return lhs;
}
+
+ @Override
+ public int getSyntaxChildCount() {
+ return 1;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ if (n == 0)
+ return lhs;
+ throw new IndexOutOfBoundsException("Elementary updates only contain 1 child");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java
index ecd4c878dfc..d1d58d62d6c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java
@@ -6,6 +6,7 @@
import de.uka.ilkd.key.ldt.JavaDLTheory;
import org.key_project.logic.Name;
+import org.key_project.logic.SyntaxElement;
import org.key_project.logic.sort.Sort;
@@ -34,4 +35,14 @@ public final class Equality extends AbstractSortedOperator {
private Equality(Name name, Sort targetSort) {
super(name, new Sort[] { targetSort, targetSort }, JavaDLTheory.FORMULA, true);
}
+
+ @Override
+ public int getSyntaxChildCount() {
+ return 0;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException(name() + " has no children");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java
index be40110ea40..a9ee0c2371b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java
@@ -6,6 +6,7 @@
import de.uka.ilkd.key.ldt.JavaDLTheory;
import org.key_project.logic.Name;
+import org.key_project.logic.SyntaxElement;
import org.key_project.logic.TermCreationException;
import org.key_project.logic.op.AbstractOperator;
import org.key_project.logic.sort.Sort;
@@ -44,4 +45,14 @@ public void validTopLevelException(T term
throw new TermCreationException(this, term);
}
}
+
+ @Override
+ public int getSyntaxChildCount() {
+ return 0;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException(name() + " has no children");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java
index a7fe9097055..bf2aabb58d0 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java
@@ -8,6 +8,7 @@
import de.uka.ilkd.key.logic.sort.ProgramSVSort;
import org.key_project.logic.Name;
+import org.key_project.logic.SyntaxElement;
import org.key_project.logic.TermCreationException;
import org.key_project.logic.op.AbstractOperator;
import org.key_project.logic.sort.Sort;
@@ -85,4 +86,14 @@ public void validTopLevelException(T term
throw new TermCreationException(this, term);
}
}
+
+ @Override
+ public int getSyntaxChildCount() {
+ return 0;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException(name() + " has no children");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java
index e2b1162c6cc..71db0f91e10 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java
@@ -6,6 +6,7 @@
import de.uka.ilkd.key.ldt.JavaDLTheory;
import org.key_project.logic.Name;
+import org.key_project.logic.SyntaxElement;
import org.key_project.logic.sort.Sort;
@@ -62,4 +63,14 @@ private static Sort[] createFormulaSortArray(int arity) {
private Junctor(Name name, int arity) {
super(name, createFormulaSortArray(arity), JavaDLTheory.FORMULA, true);
}
+
+ @Override
+ public int getSyntaxChildCount() {
+ return 0;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException("The Junctor operator " + name() + " has no children");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java
index d4e8aa5def9..c8d0769489a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java
@@ -9,6 +9,7 @@
import org.key_project.logic.Name;
import org.key_project.logic.ParsableVariable;
+import org.key_project.logic.SyntaxElement;
import org.key_project.logic.sort.Sort;
import org.key_project.util.EqualsModProofIrrelevancy;
@@ -43,4 +44,14 @@ public boolean equalsModProofIrrelevancy(Object obj) {
public int hashCodeModProofIrrelevancy() {
return Objects.hash(name(), sort());
}
+
+ @Override
+ public int getSyntaxChildCount() {
+ return 0;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException("Logic variable " + name() + " does not have children");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java
index 95d0597ab6c..adbd5d5736a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java
@@ -7,6 +7,7 @@
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
import de.uka.ilkd.key.logic.ProgramElementName;
+import org.key_project.logic.SyntaxElement;
import org.key_project.logic.sort.Sort;
import org.key_project.util.collection.ImmutableArray;
@@ -22,7 +23,7 @@
*/
public class ObserverFunction extends JFunction implements IObserverFunction {
- private final KeYJavaType container;
+ private final Qualifier container;
private final boolean isStatic;
private final ImmutableArray paramTypes;
private final KeYJavaType type;
@@ -42,7 +43,7 @@ public ObserverFunction(String baseName, Sort sort, KeYJavaType type, Sort heapS
assert type == null || type.getSort() == sort;
assert container != null;
this.type = type;
- this.container = container;
+ this.container = Qualifier.create(container);
this.isStatic = isStatic;
this.paramTypes = paramTypes;
this.heapCount = heapCount;
@@ -107,7 +108,7 @@ public final KeYJavaType getType() {
*/
@Override
public final KeYJavaType getContainerType() {
- return container;
+ return container.getQualifier();
}
@@ -169,4 +170,15 @@ public final ImmutableArray getParamTypes() {
return paramTypes;
}
+ @Override
+ public int getSyntaxChildCount() {
+ return 1;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ if (n == 0)
+ return container;
+ throw new IndexOutOfBoundsException("ObserverFunction " + name() + " has only one child");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java
index a86db464202..07a2e2bc5de 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java
@@ -257,7 +257,7 @@ public ImmutableArray getModifiers() {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
index 1ab0db5231b..12db0cb8831 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
@@ -142,7 +142,7 @@ public Expression getExpressionAt(int index) {
}
@Override
- public int getChildCount() {
+ public int getSyntaxChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java
index 40cb2da7762..49982fd749d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java
@@ -16,6 +16,7 @@
import de.uka.ilkd.key.rule.MatchConditions;
import org.key_project.logic.ParsableVariable;
+import org.key_project.logic.SyntaxElement;
import org.key_project.logic.sort.Sort;
import org.key_project.util.ExtList;
@@ -256,4 +257,15 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) {
return null;
}
}
+
+ @Override
+ public int getSyntaxChildCount() {
+ return 0;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException(
+ "Program variable " + name() + " does not have children");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
new file mode 100644
index 00000000000..be18e73d0d3
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
@@ -0,0 +1,41 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.logic.op;
+
+import java.util.WeakHashMap;
+
+import org.key_project.logic.SyntaxElement;
+
+public class Qualifier implements SyntaxElement {
+ private final T qualifier;
+
+ private static final WeakHashMap
*
- * A term label can have parameters accessible via {@link #getChild(int)} and
- * {@link #getChildCount()}. Such parameters can be any {@link Object}. But keep in mind that it is
+ * A term label can have parameters accessible via {@link #getTLChild(int)} and
+ * {@link #getTLChildCount()}. Such parameters can be any {@link Object}. But keep in mind that it is
* required to parse {@link String}s into {@link Term}s, e.g. if it is used in a Taclet definition
* or if a cut rule is applied. For convenience parameters are always printed as {@link String}s
* and have to be parsed individually into the required {@link Object} instances via a
@@ -150,7 +152,7 @@
* @see TermLabelManager
*/
// spotless:on
-public interface TermLabel extends Named {
+public interface TermLabel extends Named, SyntaxElement, /* TODO: Remove*/ TerminalSyntaxElement {
/**
* Retrieves the i-th parameter object of this term label.
@@ -161,16 +163,16 @@ public interface TermLabel extends Named {
* @param i the number of the parameter to retrieve ( {@code 0 <= i < getChildCount()})
* @return the selected parameter
* @throws IndexOutOfBoundsException if the given parameter number i is negative or
- * greater-or-equal the number of parameters returned by {@link #getChildCount()}
+ * greater-or-equal the number of parameters returned by {@link #getTLChildCount()}
*/
- Object getChild(int i);
+ Object getTLChild(int i);
/**
* Gets the number of parameters of this term label.
*
* @return the number of parameters (a non-negative number)
*/
- int getChildCount();
+ int getTLChildCount();
/**
* Returns {@code true} iff this label is used in any way during the proof. E.g.,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java
index 9ae7934762d..c4ae30a8789 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java
@@ -61,7 +61,7 @@ public UpdateableOperator lhs() {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 1;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java
index d1d58d62d6c..09fa71a855e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Equality.java
@@ -37,7 +37,7 @@ private Equality(Name name, Sort targetSort) {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/FormulaSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/FormulaSV.java
index f93b960860e..270c2a92c89 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/FormulaSV.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/FormulaSV.java
@@ -7,12 +7,13 @@
import de.uka.ilkd.key.util.pp.Layouter;
import org.key_project.logic.Name;
+import org.key_project.logic.TerminalSyntaxElement;
/**
* A schema variable that is used as placeholder for formulas.
*/
-public final class FormulaSV extends OperatorSV {
+public final class FormulaSV extends OperatorSV implements TerminalSyntaxElement {
/**
* @param name the name of the SchemaVariable
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java
index a9ee0c2371b..c7f05ada203 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfExThenElse.java
@@ -47,7 +47,7 @@ public void validTopLevelException(T term
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java
index bf2aabb58d0..a77b49ec111 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IfThenElse.java
@@ -88,7 +88,7 @@ public void validTopLevelException(T term
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java
index 71db0f91e10..42b78108d67 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Junctor.java
@@ -65,7 +65,7 @@ private Junctor(Name name, int arity) {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java
index c8d0769489a..fe94c1c3b01 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/LogicVariable.java
@@ -46,7 +46,7 @@ public int hashCodeModProofIrrelevancy() {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java
index adbd5d5736a..3edd92a4333 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ObserverFunction.java
@@ -171,7 +171,7 @@ public final ImmutableArray getParamTypes() {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 1;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java
index 07a2e2bc5de..a86db464202 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java
@@ -257,7 +257,7 @@ public ImmutableArray getModifiers() {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
index 12db0cb8831..8a0406ee4b6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
@@ -22,6 +22,8 @@
import de.uka.ilkd.key.util.pp.Layouter;
import org.key_project.logic.Name;
+import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.TerminalSyntaxElement;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
@@ -32,7 +34,7 @@
* Objects of this class are schema variables matching program constructs within modal operators.
* The particular construct being matched is determined by the ProgramSVSort of the schema variable.
*/
-public final class ProgramSV extends OperatorSV implements ProgramConstruct, UpdateableOperator {
+public final class ProgramSV extends OperatorSV implements ProgramConstruct, UpdateableOperator , TerminalSyntaxElement {
public static final Logger LOGGER = LoggerFactory.getLogger(ProgramSV.class);
private static final ProgramList EMPTY_LIST_INSTANTIATION =
@@ -142,13 +144,18 @@ public Expression getExpressionAt(int index) {
}
@Override
- public int getSyntaxChildCount() {
- return 0;
+ public ProgramElement getChildAt(int index) {
+ return this;
}
@Override
- public ProgramElement getChildAt(int index) {
- return this;
+ public SyntaxElement getChild(int n) {
+ return TerminalSyntaxElement.super.getChild(n);
+ }
+
+ @Override
+ public int getChildCount() {
+ return TerminalSyntaxElement.super.getChildCount();
}
@Override
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java
index 49982fd749d..67210bebe7f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java
@@ -259,7 +259,7 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
index be18e73d0d3..ad978c0b346 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
@@ -35,7 +35,7 @@ public SyntaxElement getChild(int n) {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java
index 7a94e63f953..e73cb2e17c6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Quantifier.java
@@ -39,7 +39,7 @@ private Quantifier(Name name) {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java
index 19bce65bc98..1cd550fa69d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java
@@ -7,6 +7,7 @@
import de.uka.ilkd.key.util.pp.Layouter;
import org.key_project.logic.Name;
+import org.key_project.logic.TerminalSyntaxElement;
import org.key_project.logic.sort.Sort;
/**
@@ -14,7 +15,7 @@
* variables have to be accompanied by a "NewDependingOn" varcond, although with the removal of the
* meta variable mechanism, this would no longer really be necessary.
*/
-public final class SkolemTermSV extends OperatorSV {
+public final class SkolemTermSV extends OperatorSV implements TerminalSyntaxElement {
/**
* Creates a new schema variable that is used as placeholder for skolem terms.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java
index 50eee4f7b96..bd675d35d89 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java
@@ -191,7 +191,7 @@ private record SortDependingFunctionTemplate(GenericSort sortDependingOn, Name k
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 1;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java
index 561389444cf..193fcc78e60 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java
@@ -76,7 +76,7 @@ public void validTopLevelException(T term
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java
index 6dc0b73105f..fc1fb8526e3 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java
@@ -8,11 +8,12 @@
import de.uka.ilkd.key.util.pp.Layouter;
import org.key_project.logic.Name;
+import org.key_project.logic.TerminalSyntaxElement;
/**
* A schema variable which matches term labels
*/
-public final class TermLabelSV extends OperatorSV implements SchemaVariable, TermLabel {
+public final class TermLabelSV extends OperatorSV implements TermLabel, TerminalSyntaxElement {
TermLabelSV(Name name) {
super(name, JavaDLTheory.TERMLABEL, true, false);
@@ -29,12 +30,12 @@ public String toString() {
}
@Override
- public Object getChild(int i) {
- throw new IndexOutOfBoundsException();
+ public int getTLChildCount() {
+ return 0;
}
@Override
- public int getSyntaxChildCount() {
- return 0;
+ public Object getTLChild(int i) {
+ throw new IndexOutOfBoundsException();
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermSV.java
index b057d045105..15353a7aaea 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermSV.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermSV.java
@@ -7,13 +7,14 @@
import de.uka.ilkd.key.util.pp.Layouter;
import org.key_project.logic.Name;
+import org.key_project.logic.TerminalSyntaxElement;
import org.key_project.logic.sort.Sort;
/**
* A schema variable that is used as placeholder for terms.
*/
-public final class TermSV extends OperatorSV {
+public final class TermSV extends OperatorSV implements TerminalSyntaxElement {
/**
* @param name the name of the schema variable
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermTransformer.java
index b722678fd3d..bb21080c5a3 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermTransformer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermTransformer.java
@@ -6,12 +6,13 @@
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.rule.inst.SVInstantiations;
+import org.key_project.logic.TerminalSyntaxElement;
/**
* TermTransformer perform complex term transformation which cannot be (efficiently or at all)
* described by taclets.
*/
-public interface TermTransformer extends org.key_project.logic.op.SortedOperator, Operator {
+public interface TermTransformer extends org.key_project.logic.op.SortedOperator, Operator, /*TODO: check*/ TerminalSyntaxElement {
/**
* initiates term transformation of term. Note the top level operator of of parameter
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateApplication.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateApplication.java
index c51f0452be3..19c503cff67 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateApplication.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateApplication.java
@@ -80,7 +80,7 @@ public static Term getTarget(Term t) {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateJunctor.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateJunctor.java
index 5f55b7cfaad..ca3586e9aa8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateJunctor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateJunctor.java
@@ -37,7 +37,7 @@ private UpdateJunctor(Name name, int arity) {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateSV.java
index 44b86cbd2c3..089f3b003e4 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateSV.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/UpdateSV.java
@@ -7,12 +7,13 @@
import de.uka.ilkd.key.util.pp.Layouter;
import org.key_project.logic.Name;
+import org.key_project.logic.TerminalSyntaxElement;
/**
* A schema variable that is used as placeholder for updates.
*/
-public final class UpdateSV extends OperatorSV {
+public final class UpdateSV extends OperatorSV implements TerminalSyntaxElement {
UpdateSV(Name name) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/VariableSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/VariableSV.java
index 1024cf7b45d..732769c23b4 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/VariableSV.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/VariableSV.java
@@ -6,12 +6,13 @@
import de.uka.ilkd.key.util.pp.Layouter;
import org.key_project.logic.Name;
+import org.key_project.logic.TerminalSyntaxElement;
import org.key_project.logic.sort.Sort;
/**
* Schema variable that is instantiated with logical variables.
*/
-public final class VariableSV extends OperatorSV implements QuantifiableVariable {
+public final class VariableSV extends OperatorSV implements QuantifiableVariable, TerminalSyntaxElement {
/**
* Creates a new SchemaVariable that is used as placeholder for bound(quantified) variables.
@@ -34,4 +35,6 @@ public void layout(Layouter> l) {
l.print("\\schemaVar \\variables ").print(sort().name().toString()).print(" ")
.print(name().toString());
}
+
+
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java
index 04c17871eea..4f344bb86a2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java
@@ -482,7 +482,7 @@ protected boolean canStandFor(ProgramElement pe, Services services) {
|| pe instanceof SeqLength || pe instanceof SeqGet || pe instanceof SeqIndexOf
|| pe instanceof SeqSub || pe instanceof SeqReverse || pe instanceof SeqPut) {
if (pe instanceof NonTerminalProgramElement npe) {
- for (int i = 0, childCount = npe.getSyntaxChildCount(); i < childCount; i++) {
+ for (int i = 0, childCount = npe.getChildCount(); i < childCount; i++) {
if (!canStandFor(npe.getChildAt(i), services)) {
return false;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
index 409c6dd32cd..11deca874c7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
@@ -816,11 +816,11 @@ void printLabels(Term t, String left, String right) {
afterFirst = true;
}
layouter.print(l.name().toString());
- if (l.getChildCount() > 0) {
+ if (l.getTLChildCount() > 0) {
layouter.print("(").beginC();
- for (int i = 0; i < l.getChildCount(); i++) {
- layouter.print("\"" + l.getChild(i).toString() + "\"");
- if (i < l.getChildCount() - 1) {
+ for (int i = 0; i < l.getTLChildCount(); i++) {
+ layouter.print("\"" + l.getTLChild(i).toString() + "\"");
+ if (i < l.getTLChildCount() - 1) {
layouter.print(",").ind(1, 2);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java
index fbc296e5837..aa4d5c176c9 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java
@@ -410,7 +410,7 @@ public void performActionOnDLEmbeddedExpression(DLEmbeddedExpression x) {
layouter.print("\\dl_" + x.getFunctionSymbol().name());
layouter.print("(");
- for (int i = 0; i < x.getSyntaxChildCount(); i++) {
+ for (int i = 0; i < x.getChildCount(); i++) {
if (i != 0) {
layouter.print(",").brk();
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java
index 1f0aebea363..b8fcfbee6b9 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java
@@ -314,7 +314,7 @@ private ImmutableList getJavaTacletList(
if (pe instanceof ProgramPrefix) {
int next = prefixOccurrences.occurred(pe);
NonTerminalProgramElement nt = (NonTerminalProgramElement) pe;
- if (next < nt.getSyntaxChildCount()) {
+ if (next < nt.getChildCount()) {
return getJavaTacletList(map, nt.getChildAt(next), prefixOccurrences);
}
} else {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopInvariantBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopInvariantBuiltInRuleApp.java
index bfd4ff80c55..88f44e40120 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopInvariantBuiltInRuleApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopInvariantBuiltInRuleApp.java
@@ -93,7 +93,7 @@ private LoopSpecification instantiateIndexValues(LoopSpecification rawInv,
// try to retrieve a loop index variable
de.uka.ilkd.key.java.statement.IGuard guard = loop.getGuard();
// the guard is expected to be of the form "i < x" and we want to retrieve "i".
- assert guard.getSyntaxChildCount() == 1 : "child count: " + guard.getSyntaxChildCount();
+ assert guard.getChildCount() == 1 : "child count: " + guard.getChildCount();
ProgramElement guardStatement = guard.getChildAt(0);
skipIndex = !(guardStatement instanceof LessThan);
Expression loopIndex =
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java
index ca3e68b6a44..74f87909a8f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java
@@ -55,7 +55,7 @@ public MatchConditions check(SchemaVariable sv, SVSubstitute instCandidate,
assert !instantiatedTerm.javaBlock().isEmpty();
assert instantiatedTerm.javaBlock().program() instanceof StatementBlock;
- assert ((StatementBlock) instantiatedTerm.javaBlock().program()).getSyntaxChildCount() == 1;
+ assert ((StatementBlock) instantiatedTerm.javaBlock().program()).getChildCount() == 1;
return matchCond.setInstantiations(//
svInst.add(storeInSV,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java
index 3fc16ba6428..9b964549cfb 100755
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java
@@ -129,8 +129,8 @@ private Set collectSubtermOrigins(Term term, Set result) {
TermLabel label = term.getLabel(OriginTermLabel.NAME);
if (label != null) {
- result.add((Origin) label.getChild(0));
- result.addAll((Set) label.getChild(1));
+ result.add((Origin) label.getTLChild(0));
+ result.addAll((Set) label.getTLChild(1));
}
ImmutableArray subterms = term.subs();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ProgramTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ProgramTransformer.java
index fd5edcccdb6..0b7e5d2716e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ProgramTransformer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ProgramTransformer.java
@@ -134,7 +134,7 @@ public Statement getStatementAt(int index) {
*
* @return an int giving the number of children of this node
*/
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 1;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileLoopTransformation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileLoopTransformation.java
index a11be238695..14bc6a66ec1 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileLoopTransformation.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileLoopTransformation.java
@@ -718,11 +718,11 @@ public void performActionOnMethodFrame(MethodFrame x) {
ExtList changeList = stack.peek();
if (!changeList.isEmpty() && changeList.getFirst() == CHANGED) {
changeList.removeFirst();
- if (x.getSyntaxChildCount() == 3) {
+ if (x.getChildCount() == 3) {
addChild(KeYJavaASTFactory.methodFrame((IProgramVariable) changeList.get(0),
(IExecutionContext) changeList.get(1), (StatementBlock) changeList.get(2),
PositionInfo.UNDEFINED));
- } else if (x.getSyntaxChildCount() == 2) {
+ } else if (x.getChildCount() == 2) {
addChild(KeYJavaASTFactory.methodFrame((IExecutionContext) changeList.get(0),
(StatementBlock) changeList.get(1), PositionInfo.UNDEFINED));
} else {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
index 00be8ef33e4..15fba88cfc9 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
@@ -281,7 +281,7 @@ public ImmutableSet extractClassSpecs(KeYJavaType kjt)
}
// iterate over all children
- for (int i = 0, n = td.getSyntaxChildCount(); i <= n; i++) {
+ for (int i = 0, n = td.getChildCount(); i <= n; i++) {
// collect comments
// (last position are comments of type declaration itself)
Comment[] comments = null;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java
index 76edd2ab297..44fb3a27177 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java
@@ -8,11 +8,12 @@
import org.key_project.logic.Name;
import org.key_project.logic.ParsableVariable;
+import org.key_project.logic.TerminalSyntaxElement;
import org.key_project.logic.sort.Sort;
@Deprecated
public final class Metavariable extends AbstractSortedOperator
- implements ParsableVariable, Comparable {
+ implements ParsableVariable, Comparable, TerminalSyntaxElement {
// Used to define an alternative order of all existing
// metavariables
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java
index c3a3b2599d0..201090e5703 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java
@@ -19,6 +19,7 @@
import org.key_project.logic.Name;
import org.key_project.logic.TermCreationException;
+import org.key_project.logic.TerminalSyntaxElement;
import org.key_project.logic.op.Modifier;
import org.key_project.logic.op.SortedOperator;
import org.key_project.logic.sort.Sort;
@@ -95,7 +96,7 @@ protected Term generateOneTerm(Term superterm, int child) {
return services.getTermBuilder().tf().createTerm(binFunc, superterm, index);
}
- private static class SuperTermGeneratedOp implements SortedOperator, Operator {
+ private static class SuperTermGeneratedOp implements SortedOperator, Operator, TerminalSyntaxElement {
private final Name NAME;
private final IntegerLDT numbers;
diff --git a/key.core/src/test/java/de/uka/ilkd/key/java/TestContextStatementBlock.java b/key.core/src/test/java/de/uka/ilkd/key/java/TestContextStatementBlock.java
index 68cd906b2d0..b7f699eeff2 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/java/TestContextStatementBlock.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/java/TestContextStatementBlock.java
@@ -43,7 +43,7 @@ public void tearDown() {
public void testContextTermInstantiation() {
ExtList statementList = new ExtList();
StatementBlock stContainer = (StatementBlock) blockOne.program();
- int size = stContainer.getSyntaxChildCount();
+ int size = stContainer.getChildCount();
assertEquals(3, size, "Wrong size. Should have only 3 children");
PosInProgram prefixEnd = PosInProgram.TOP.down(0);
assertTrue(
diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java
index 517a5a78a8c..8599f8d81d3 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java
@@ -557,18 +557,18 @@ public void testParseLabel() throws TermLabelException {
TermLabel label = manager.parseLabel("ONE", null, services);
assertTrue(label instanceof LoggingTermLabel);
assertEquals("ONE", label.name().toString());
- assertEquals(0, label.getChildCount());
+ assertEquals(0, label.getTLChildCount());
// Test empty parameter
label = manager.parseLabel("TWO", null, services);
assertTrue(label instanceof LoggingTermLabel);
assertEquals("TWO", label.name().toString());
- assertEquals(0, label.getChildCount());
+ assertEquals(0, label.getTLChildCount());
// Test with parameter
label = manager.parseLabel("THREE", Collections.singletonList("Param"), services);
assertTrue(label instanceof LoggingTermLabel);
assertEquals("THREE", label.name().toString());
- assertEquals(1, label.getChildCount());
- assertEquals("Param", label.getChild(0));
+ assertEquals(1, label.getTLChildCount());
+ assertEquals("Param", label.getTLChild(0));
// Test unsupported
try {
manager.parseLabel("UNKNOWN", null, services);
@@ -850,12 +850,12 @@ public Name name() {
}
@Override
- public Object getChild(int i) {
+ public Object getTLChild(int i) {
return arguments.get(i);
}
@Override
- public int getChildCount() {
+ public int getTLChildCount() {
return arguments != null ? arguments.size() : 0;
}
}
diff --git a/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java b/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java
index 2439237ae9e..a0e61d60102 100644
--- a/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java
+++ b/key.ncore/src/main/java/org/key_project/logic/SyntaxElement.java
@@ -21,5 +21,5 @@ public interface SyntaxElement {
*
* @return the number of children of this syntax element.
*/
- int getSyntaxChildCount();
+ int getChildCount();
}
diff --git a/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java
index b6b20313bbe..cc4892122b3 100644
--- a/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java
+++ b/key.ncore/src/main/java/org/key_project/logic/SyntaxElementCursor.java
@@ -22,7 +22,7 @@ public SyntaxElement getCurrentNode() {
}
public boolean gotoFirstChild() {
- if (node.getSyntaxChildCount() <= 0)
+ if (node.getChildCount() <= 0)
return false;
path.push(new ParentAndPosition(node, 0));
node = node.getChild(0);
@@ -35,7 +35,7 @@ public boolean gotoNextSibling() {
var pnp = path.pop();
SyntaxElement parent = pnp.parent;
int index = pnp.index + 1;
- if (index > parent.getSyntaxChildCount()) {
+ if (index > parent.getChildCount()) {
return false;
}
path.push(new ParentAndPosition(parent, index));
diff --git a/key.ncore/src/main/java/org/key_project/logic/Term.java b/key.ncore/src/main/java/org/key_project/logic/Term.java
index a66d82ecc52..5dc16e0ea29 100644
--- a/key.ncore/src/main/java/org/key_project/logic/Term.java
+++ b/key.ncore/src/main/java/org/key_project/logic/Term.java
@@ -93,7 +93,7 @@ public interface Term extends LogicElement, Sorted {
void execPreOrder(Visitor visitor);
@Override
- default int getSyntaxChildCount() {
+ default int getChildCount() {
return 1 + boundVars().size() + subs().size();
}
@@ -108,6 +108,6 @@ default SyntaxElement getChild(int n) {
if (n < subs().size())
return sub(n);
throw new IndexOutOfBoundsException(
- "Term " + this + " has only " + getSyntaxChildCount() + " children");
+ "Term " + this + " has only " + getChildCount() + " children");
}
}
diff --git a/key.ncore/src/main/java/org/key_project/logic/TerminalSyntaxElement.java b/key.ncore/src/main/java/org/key_project/logic/TerminalSyntaxElement.java
new file mode 100644
index 00000000000..e6d25f7ae00
--- /dev/null
+++ b/key.ncore/src/main/java/org/key_project/logic/TerminalSyntaxElement.java
@@ -0,0 +1,13 @@
+package org.key_project.logic;
+
+public interface TerminalSyntaxElement extends SyntaxElement{
+ @Override
+ default SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException(this.getClass() + " " + this + " has no children");
+ }
+
+ @Override
+ default int getChildCount() {
+ return 0;
+ }
+}
diff --git a/key.ncore/src/main/java/org/key_project/logic/op/Function.java b/key.ncore/src/main/java/org/key_project/logic/op/Function.java
index 1f638f9efd8..ec55b5dcd44 100644
--- a/key.ncore/src/main/java/org/key_project/logic/op/Function.java
+++ b/key.ncore/src/main/java/org/key_project/logic/op/Function.java
@@ -54,7 +54,7 @@ public final String toString() {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.ncore/src/main/java/org/key_project/logic/op/Modality.java b/key.ncore/src/main/java/org/key_project/logic/op/Modality.java
index 4a6c01643e3..9df6dccc9bd 100644
--- a/key.ncore/src/main/java/org/key_project/logic/op/Modality.java
+++ b/key.ncore/src/main/java/org/key_project/logic/op/Modality.java
@@ -43,7 +43,7 @@ public final K kind() {
public abstract Program program();
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 2;
}
@@ -92,7 +92,7 @@ public int hashCode() {
}
@Override
- public int getSyntaxChildCount() {
+ public int getChildCount() {
return 0;
}
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java
index 0de19c95623..1ee7b710b81 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java
@@ -815,7 +815,7 @@ private static PositionInfo joinPositionsRec(SourceElement se) {
PositionInfo pos = se.getPositionInfo();
- for (int i = 0; i < ntpe.getSyntaxChildCount(); i++) {
+ for (int i = 0; i < ntpe.getChildCount(); i++) {
ProgramElement pe2 = ntpe.getChildAt(i);
pos = PositionInfo.join(pos, joinPositionsRec(pe2));
}
From 1bb54fc29654174f1d0e4d80621ac9b403b634f0 Mon Sep 17 00:00:00 2001
From: Drodt
Date: Wed, 22 May 2024 10:47:36 +0200
Subject: [PATCH 06/11] Clean up inheritance
---
.../key/java/JavaNonTerminalProgramElement.java | 5 -----
.../key/java/NonTerminalProgramElement.java | 6 ++++++
.../ilkd/key/java/TerminalProgramElement.java | 11 ++---------
.../uka/ilkd/key/java/declaration/Modifier.java | 13 ++++++++++++-
.../key/java/declaration/modifier/Static.java | 1 +
.../ilkd/key/java/statement/IForUpdates.java | 2 +-
.../uka/ilkd/key/java/statement/ILoopInit.java | 3 ++-
.../de/uka/ilkd/key/logic/op/ProgramSV.java | 6 +++---
.../de/uka/ilkd/key/logic/op/Qualifier.java | 13 ++-----------
.../java/org/key_project/logic/op/Modality.java | 17 ++---------------
10 files changed, 31 insertions(+), 46 deletions(-)
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java
index 8a1b4c0cf82..4f1dfdb2ff2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java
@@ -164,9 +164,4 @@ protected MatchConditions matchChildren(SourceData source, MatchConditions match
return matchCond;
}
-
- @Override
- public SyntaxElement getChild(int n) {
- return getChildAt(n);
- }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java
index ca20a719d4d..1865f6e964c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java
@@ -3,6 +3,8 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.java;
+import org.key_project.logic.SyntaxElement;
+
/**
* Non terminal program element. taken from COMPOST and changed to achieve an immutable structure
*/
@@ -25,4 +27,8 @@ public interface NonTerminalProgramElement extends ProgramElement {
*/
ProgramElement getChildAt(int index);
+ @Override
+ default SyntaxElement getChild(int n) {
+ return getChildAt(n);
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java
index 653187dc473..d240ddafb2e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java
@@ -4,19 +4,12 @@
package de.uka.ilkd.key.java;
import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.TerminalSyntaxElement;
/**
* Terminal program element. taken from COMPOST and changed to achieve an immutable structure
*/
-public interface TerminalProgramElement extends ProgramElement {
- @Override
- default int getChildCount() {
- return 0;
- }
+public interface TerminalProgramElement extends ProgramElement, TerminalSyntaxElement {
- @Override
- default SyntaxElement getChild(int n) {
- throw new IndexOutOfBoundsException("Program element " + this + " has no children");
- }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java
index 357d417d3ca..c6533ebfe38 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java
@@ -7,13 +7,14 @@
import de.uka.ilkd.key.java.TerminalProgramElement;
import de.uka.ilkd.key.java.visitor.Visitor;
+import org.key_project.logic.SyntaxElement;
import org.key_project.util.ExtList;
/**
* Modifier. taken from COMPOST and changed to achieve an immutable structure
*/
-public abstract class Modifier extends JavaProgramElement implements TerminalProgramElement {
+public abstract class Modifier extends JavaProgramElement {
/**
* Modifier.
@@ -56,4 +57,14 @@ public String getText() {
public void visit(Visitor v) {
v.performActionOnModifier(this);
}
+
+ @Override
+ public int getChildCount() {
+ return 0;
+ }
+
+ @Override
+ public SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException(getClass() + " " + this + " has no children");
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Static.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Static.java
index 6efc4cf1f20..f99f1494181 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Static.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Static.java
@@ -5,6 +5,7 @@
import de.uka.ilkd.key.java.declaration.Modifier;
+import org.key_project.logic.TerminalSyntaxElement;
import org.key_project.util.ExtList;
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java
index a532522aa5e..75d499d1cdf 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java
@@ -7,7 +7,7 @@
import org.key_project.util.collection.ImmutableArray;
-public interface IForUpdates extends de.uka.ilkd.key.java.TerminalProgramElement {
+public interface IForUpdates extends de.uka.ilkd.key.java.NonTerminalProgramElement {
int size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java
index c8528112d4d..362b5b85e4a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java
@@ -4,11 +4,12 @@
package de.uka.ilkd.key.java.statement;
import de.uka.ilkd.key.java.LoopInitializer;
+import de.uka.ilkd.key.java.NonTerminalProgramElement;
import de.uka.ilkd.key.java.TerminalProgramElement;
import org.key_project.util.collection.ImmutableArray;
-public interface ILoopInit extends TerminalProgramElement {
+public interface ILoopInit extends NonTerminalProgramElement {
int size();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
index 8a0406ee4b6..efd705956fc 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
@@ -34,7 +34,7 @@
* Objects of this class are schema variables matching program constructs within modal operators.
* The particular construct being matched is determined by the ProgramSVSort of the schema variable.
*/
-public final class ProgramSV extends OperatorSV implements ProgramConstruct, UpdateableOperator , TerminalSyntaxElement {
+public final class ProgramSV extends OperatorSV implements ProgramConstruct, UpdateableOperator , SyntaxElement {
public static final Logger LOGGER = LoggerFactory.getLogger(ProgramSV.class);
private static final ProgramList EMPTY_LIST_INSTANTIATION =
@@ -150,12 +150,12 @@ public ProgramElement getChildAt(int index) {
@Override
public SyntaxElement getChild(int n) {
- return TerminalSyntaxElement.super.getChild(n);
+ throw new IndexOutOfBoundsException("ProgramSV " + this + " has no children");
}
@Override
public int getChildCount() {
- return TerminalSyntaxElement.super.getChildCount();
+ return 0;
}
@Override
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
index ad978c0b346..ed06827732d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
@@ -6,8 +6,9 @@
import java.util.WeakHashMap;
import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.TerminalSyntaxElement;
-public class Qualifier implements SyntaxElement {
+public class Qualifier implements TerminalSyntaxElement {
private final T qualifier;
private static final WeakHashMap