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
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java
index c6084f2b8fb..d997436ad8e 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java
+++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java
@@ -32,6 +32,7 @@
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
+import org.key_project.logic.SyntaxElement;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
@@ -76,7 +77,7 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea
* A {@link Map} mapping from relevant variables for the condition to their runtime equivalent
* in KeY
*/
- private Map variableNamingMap;
+ private Map variableNamingMap;
/**
* The list of parameter variables of the method that contains the associated breakpoint
@@ -162,14 +163,14 @@ private void putValuesFromGlobalVars(ProgramVariable varForCondition, Node node,
*
* @return the cloned map
*/
- private Map getOldMap() {
- Map oldMap = new HashMap<>();
- for (Entry svSubstituteSVSubstituteEntry : getVariableNamingMap()
+ private Map getOldMap() {
+ Map oldMap = new HashMap<>();
+ for (Entry svSubstituteSVSubstituteEntry : getVariableNamingMap()
.entrySet()) {
Entry, ?> oldEntry = svSubstituteSVSubstituteEntry;
- if (oldEntry.getKey() instanceof SVSubstitute
- && oldEntry.getValue() instanceof SVSubstitute) {
- oldMap.put((SVSubstitute) oldEntry.getKey(), (SVSubstitute) oldEntry.getValue());
+ if (oldEntry.getKey() instanceof SyntaxElement
+ && oldEntry.getValue() instanceof SyntaxElement) {
+ oldMap.put((SyntaxElement) oldEntry.getKey(), (SyntaxElement) oldEntry.getValue());
}
}
return oldMap;
@@ -200,7 +201,7 @@ private void freeVariablesAfterReturn(Node node, RuleApp ruleApp, boolean inScop
* @param oldMap the oldMap variableNamings
*/
private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, boolean inScope,
- Map oldMap, RuleApp ruleApp) {
+ Map oldMap, RuleApp ruleApp) {
// look for renamings KeY did
boolean found = false;
// get current renaming tables
@@ -215,7 +216,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
.getHashMap().entrySet()) {
Entry, ?> entry = value;
if (entry.getKey() instanceof LocationVariable
- && entry.getValue() instanceof SVSubstitute) {
+ && entry.getValue() instanceof SyntaxElement) {
if ((VariableNamer.getBasename(((LocationVariable) entry.getKey()).name()))
.equals(varForCondition.name())
&& ((LocationVariable) entry.getKey()).name().toString()
@@ -229,7 +230,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
// add new value
toKeep.add((LocationVariable) entry.getValue());
getVariableNamingMap().put(varForCondition,
- (SVSubstitute) entry.getValue());
+ (SyntaxElement) entry.getValue());
found = true;
break;
} else if (inScope && ((LocationVariable) entry.getKey()).name()
@@ -242,7 +243,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
// add new value
toKeep.add((LocationVariable) entry.getValue());
getVariableNamingMap().put(varForCondition,
- (SVSubstitute) entry.getValue());
+ (SyntaxElement) entry.getValue());
found = true;
break;
}
@@ -263,7 +264,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
protected void refreshVarMaps(RuleApp ruleApp, Node node) {
boolean inScope = isInScope(node);
// collect old values
- Map oldMap = getOldMap();
+ Map oldMap = getOldMap();
// put values into map which have to be replaced
for (ProgramVariable varForCondition : getVarsForCondition()) {
// put global variables only done when a variable is instantiated by
@@ -498,14 +499,14 @@ public Set getToKeep() {
/**
* @return the variableNamingMap
*/
- public Map getVariableNamingMap() {
+ public Map getVariableNamingMap() {
return variableNamingMap;
}
/**
* @param variableNamingMap the variableNamingMap to set
*/
- public void setVariableNamingMap(Map variableNamingMap) {
+ public void setVariableNamingMap(Map variableNamingMap) {
this.variableNamingMap = variableNamingMap;
}
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..60221fca8fe 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 getChildCount() {
+ 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/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/SourceElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java
index 046d51538cb..206efd7fb8e 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
@@ -4,7 +4,8 @@
package de.uka.ilkd.key.java;
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
@@ -12,7 +13,7 @@
* to achieve an immutable structure
*/
-public interface SourceElement extends SVSubstitute {
+public interface SourceElement extends SyntaxElement {
/**
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..e6fdc309f71 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,12 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.java;
+import org.key_project.logic.TerminalSyntaxElement;
+
/**
* Terminal program element. taken from COMPOST and changed to achieve an immutable structure
*/
-public interface TerminalProgramElement extends ProgramElement {
+public interface TerminalProgramElement extends ProgramElement, TerminalSyntaxElement {
+
}
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..fc59c65e880 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,7 +163,7 @@ public SourceElement getFirstElement() {
@Override
public SourceElement getLastElement() {
- return getChildAt(getChildCount() - 1).getLastElement();
+ return getChildAt(this.getChildCount() - 1).getLastElement();
}
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..b8fd1e2d410 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
@@ -4,16 +4,16 @@
package de.uka.ilkd.key.java.declaration;
import de.uka.ilkd.key.java.JavaProgramElement;
-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 +56,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/expression/operator/Instanceof.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Instanceof.java
index 284c254db72..d53c134154e 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.getChildCount() == 2 : "not 2 children but " + this.getChildCount();
}
public Instanceof(Expression unaryChild, TypeReference typeref) {
super(unaryChild, typeref);
- assert getChildCount() == 2 : "not 2 children but " + getChildCount();
+ assert this.getChildCount() == 2 : "not 2 children but " + this.getChildCount();
}
/**
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..6d041245c71 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.getChildCount() - 1).getLastElement();
}
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..ee0bc657b95 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,11 @@
package de.uka.ilkd.key.java.statement;
import de.uka.ilkd.key.java.LoopInitializer;
-import de.uka.ilkd.key.java.TerminalProgramElement;
+import de.uka.ilkd.key.java.NonTerminalProgramElement;
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/java/statement/LoopScopeBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java
index 90b373e1438..60d71b65f31 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.getChildCount() - 1).down(0);
}
/**
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..105e3ab446a 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(getChildCount() - 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(getChildCount() - 1).down(0);
Debug.assertTrue(execContext != null, "methodframe: executioncontext missing");
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..02386a7c6e9 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.getChildCount() - 1).getLastElement();
}
/**
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..9f18163e5e7 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;
@@ -128,4 +129,18 @@ public int hashCodeModProofIrrelevancy() {
}
return hashCode;
}
+
+ @Override
+ public int getChildCount() {
+ 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/ProgramConstruct.java b/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramConstruct.java
index 70bd980e18b..8b68b44f4dc 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramConstruct.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramConstruct.java
@@ -18,6 +18,8 @@
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.logic.op.IProgramVariable;
+import org.key_project.logic.SyntaxElement;
+
/**
* A type that implement this interface can be used in all java programs instead of an expression or
* statement. For example class SchemaVariable implements this interface to be able to stand for
@@ -26,4 +28,9 @@
public interface ProgramConstruct extends Expression, Statement, ILoopInit, IForUpdates, IGuard,
Label, TerminalProgramElement, ExpressionStatement, TypeReference, IProgramVariable,
IProgramMethod, Branch, IExecutionContext, MethodName {
+ @Override
+ SyntaxElement getChild(int n);
+
+ @Override
+ int getChildCount();
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Term.java b/key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
index 60c03e6fdae..73e99f387e2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
@@ -8,7 +8,6 @@
import de.uka.ilkd.key.logic.label.TermLabel;
import de.uka.ilkd.key.logic.op.Operator;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
import org.key_project.logic.Name;
import org.key_project.logic.Visitor;
@@ -43,7 +42,7 @@
* supported: {@link Term#execPostOrder(Visitor)} and {@link Term#execPreOrder(Visitor)}.
*/
public interface Term
- extends SVSubstitute, Sorted, TermEqualsModProperty, org.key_project.logic.Term {
+ extends Sorted, TermEqualsModProperty, org.key_project.logic.Term {
@Override
Operator op();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java
index c4181e3c988..f4cb02f511f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java
@@ -40,7 +40,7 @@ public ProgramVariable exceptionVariable() {
* {@inheritDoc}
*/
@Override
- public ProgramVariable getChild(int i) {
+ public ProgramVariable getTLChild(int i) {
if (i == 0) {
return exceptionVariable();
}
@@ -51,7 +51,7 @@ public ProgramVariable getChild(int i) {
* {@inheritDoc}
*/
@Override
- public int getChildCount() {
+ public int getTLChildCount() {
return 1;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java
index cde4271a90d..def77a6dd50 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java
@@ -134,7 +134,7 @@ public String toString() {
* {@inheritDoc}
*/
@Override
- public Object getChild(int i) {
+ public Object getTLChild(int i) {
return switch (i) {
case 0 -> getId();
case 1 -> beforeIds;
@@ -146,7 +146,7 @@ public Object getChild(int i) {
* {@inheritDoc}
*/
@Override
- public int getChildCount() {
+ public int getTLChildCount() {
if (beforeIds != null) {
return 2;
} else {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java
index 1e3edea26ed..f65285f1849 100755
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java
@@ -57,7 +57,7 @@ public class OriginTermLabel implements TermLabel {
public final static Name NAME = new Name("origin");
/**
- * @see #getChildCount()
+ * @see #getTLChildCount()
*/
public final static int CHILD_COUNT = 2;
public static final Sort[] EMPTY_SORTS = new Sort[0];
@@ -450,7 +450,7 @@ public Name name() {
}
@Override
- public Object getChild(int i) {
+ public Object getTLChild(int i) {
if (i == 0) {
return origin;
} else if (i == 1) {
@@ -461,7 +461,7 @@ public Object getChild(int i) {
}
@Override
- public int getChildCount() {
+ public int getTLChildCount() {
return CHILD_COUNT;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java
index 850c5c1b3d5..596410ce3e8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java
@@ -139,7 +139,7 @@ public Name name() {
* {@link IndexOutOfBoundsException}.
*/
@Override
- public Object getChild(int i) {
+ public Object getTLChild(int i) {
throw new IndexOutOfBoundsException();
}
@@ -150,7 +150,7 @@ public Object getChild(int i) {
* Simple term labels have no parameters. This always returns 0.
*/
@Override
- public int getChildCount() {
+ public int getTLChildCount() {
return 0;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabel.java
index 03659186d6a..6596ce2ba89 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabel.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabel.java
@@ -50,7 +50,7 @@ public String toString() {
* {@inheritDoc}
*/
@Override
- public Object getChild(int i) {
+ public Object getTLChild(int i) {
if (i == 0) {
return id();
}
@@ -61,7 +61,7 @@ public Object getChild(int i) {
* {@inheritDoc}
*/
@Override
- public int getChildCount() {
+ public int getTLChildCount() {
return 1;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java
index b514fbd04d5..a5287c1f2d1 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java
@@ -20,6 +20,8 @@
import org.key_project.logic.Name;
import org.key_project.logic.Named;
+import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.TerminalSyntaxElement;
// spotless:off // this protects the JavaDoc from automatic reformatting
/**
@@ -34,8 +36,8 @@
* without parameters class {@link ParameterlessTermLabel} can be used.
*
*
- * 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 0837fda6089..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
@@ -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 getChildCount() {
+ 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..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
@@ -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 getChildCount() {
+ 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/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 be40110ea40..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
@@ -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 getChildCount() {
+ 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..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
@@ -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 getChildCount() {
+ 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..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
@@ -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 getChildCount() {
+ 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..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
@@ -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 getChildCount() {
+ 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/Modality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java
index 0510d66fc73..c9d4557970b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java
@@ -125,7 +125,7 @@ public String toString() {
return super.toString();
}
- public static class JavaModalityKind extends Kind implements SVSubstitute {
+ public static class JavaModalityKind extends Kind {
private static final Map kinds = new HashMap<>();
/**
* The diamond operator of dynamic logic. A formula Phi can be read as after
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..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
@@ -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 getChildCount() {
+ 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/Operator.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Operator.java
index e12cfc522c6..3647725e850 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Operator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Operator.java
@@ -13,7 +13,7 @@
* etc. have to implement this interface.
*/
public interface Operator
- extends org.key_project.logic.op.Operator, SVSubstitute, EqualsModProofIrrelevancy {
+ extends org.key_project.logic.op.Operator, EqualsModProofIrrelevancy {
/**
* comparator to compare operators; for modalities only their kind is compared
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 0a4733e4792..0d43f11b6e9 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,7 @@
import de.uka.ilkd.key.util.pp.Layouter;
import org.key_project.logic.Name;
+import org.key_project.logic.SyntaxElement;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
@@ -32,7 +33,8 @@
* 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, SyntaxElement {
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 getChildCount() {
- return 0;
+ public ProgramElement getChildAt(int index) {
+ return this;
}
@Override
- public ProgramElement getChildAt(int index) {
- return this;
+ public SyntaxElement getChild(int n) {
+ throw new IndexOutOfBoundsException("ProgramSV " + this + " has no children");
+ }
+
+ @Override
+ public int getChildCount() {
+ return 0;
}
@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 40cb2da7762..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
@@ -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 getChildCount() {
+ 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..2450b036d2e
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
@@ -0,0 +1,31 @@
+/* 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.TerminalSyntaxElement;
+
+public class Qualifier implements TerminalSyntaxElement {
+ private final T qualifier;
+
+ private static final WeakHashMap