From 81d3120159241810108372a6a780893c9a5f8b12 Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 22 May 2024 10:59:03 +0200 Subject: [PATCH] Remove SVSubstitute --- .../AbstractConditionalBreakpoint.java | 29 ++++++++++--------- .../java/JavaNonTerminalProgramElement.java | 1 - .../de/uka/ilkd/key/java/SourceElement.java | 3 +- .../ilkd/key/java/TerminalProgramElement.java | 1 - .../ilkd/key/java/declaration/Modifier.java | 1 - .../key/java/declaration/modifier/Static.java | 1 - .../ilkd/key/java/statement/ILoopInit.java | 1 - .../uka/ilkd/key/logic/ProgramConstruct.java | 3 +- .../main/java/de/uka/ilkd/key/logic/Term.java | 3 +- .../uka/ilkd/key/logic/label/TermLabel.java | 2 +- .../de/uka/ilkd/key/logic/op/Modality.java | 2 +- .../de/uka/ilkd/key/logic/op/Operator.java | 2 +- .../de/uka/ilkd/key/logic/op/ProgramSV.java | 4 +-- .../de/uka/ilkd/key/logic/op/Qualifier.java | 1 - .../uka/ilkd/key/logic/op/SVSubstitute.java | 12 -------- .../ilkd/key/logic/op/TermTransformer.java | 4 ++- .../de/uka/ilkd/key/logic/op/VariableSV.java | 3 +- .../de/uka/ilkd/key/proof/OpReplacer.java | 12 ++++---- .../de/uka/ilkd/key/proof/ReplacementMap.java | 13 +++++---- .../de/uka/ilkd/key/rule/TacletMatcher.java | 5 ++-- .../uka/ilkd/key/rule/VariableCondition.java | 6 ++-- .../key/rule/VariableConditionAdapter.java | 7 +++-- .../conditions/AbstractOrInterfaceType.java | 4 +-- .../AlternativeVariableCondition.java | 5 ++-- .../ApplyUpdateOnRigidCondition.java | 4 ++- .../ArrayComponentTypeCondition.java | 4 +-- .../rule/conditions/ArrayLengthCondition.java | 5 ++-- .../rule/conditions/ArrayTypeCondition.java | 4 +-- .../rule/conditions/ConstantCondition.java | 5 ++-- .../ContainsAssignmentCondition.java | 5 ++-- .../key/rule/conditions/DifferentFields.java | 4 +-- .../DifferentInstantiationCondition.java | 4 +-- .../DropEffectlessElementariesCondition.java | 6 ++-- .../DropEffectlessStoresCondition.java | 5 ++-- .../conditions/EnumConstantCondition.java | 5 ++-- .../rule/conditions/EnumTypeCondition.java | 4 +-- .../rule/conditions/EqualUniqueCondition.java | 4 ++- .../conditions/FieldTypeToSortCondition.java | 3 +- .../conditions/FinalReferenceCondition.java | 5 ++-- .../FreeLabelInVariableCondition.java | 5 ++-- .../conditions/HasLoopInvariantCondition.java | 5 ++-- .../ilkd/key/rule/conditions/InStrictFp.java | 5 ++-- .../rule/conditions/IsLabeledCondition.java | 5 ++-- .../key/rule/conditions/IsThisReference.java | 4 +-- .../conditions/JavaTypeToSortCondition.java | 4 +-- .../conditions/LocalVariableCondition.java | 5 ++-- .../LoopFreeInvariantCondition.java | 5 ++-- .../conditions/LoopInvariantCondition.java | 5 ++-- .../rule/conditions/LoopVariantCondition.java | 5 ++-- .../conditions/MayExpandMethodCondition.java | 4 +-- .../conditions/MetaDisjointCondition.java | 3 +- .../rule/conditions/ModelFieldCondition.java | 5 ++-- .../conditions/NewJumpLabelCondition.java | 6 ++-- .../rule/conditions/ObserverCondition.java | 6 ++-- .../conditions/SameObserverCondition.java | 5 ++-- .../SimplifyIfThenElseUpdateCondition.java | 4 ++- .../rule/conditions/StaticFieldCondition.java | 4 ++- .../conditions/StaticMethodCondition.java | 4 +-- .../conditions/StaticReferenceCondition.java | 5 ++-- .../rule/conditions/StoreStmtInCondition.java | 5 ++-- .../rule/conditions/StoreTermInCondition.java | 5 ++-- .../rule/conditions/SubFormulaCondition.java | 5 ++-- .../rule/conditions/TermLabelCondition.java | 4 +-- .../conditions/TypeComparisonCondition.java | 4 +-- .../key/rule/conditions/TypeCondition.java | 4 +-- .../key/rule/conditions/TypeResolver.java | 26 ++++++++--------- .../uka/ilkd/key/rule/inst/ProgramList.java | 14 +++++++-- .../key/rule/match/vm/VMTacletMatcher.java | 8 ++--- .../key/speclang/DependencyContractImpl.java | 14 ++++----- .../FunctionalOperationContractImpl.java | 11 +++---- .../ilkd/key/speclang/LoopContractImpl.java | 4 +-- .../uka/ilkd/key/speclang/ReplacementMap.java | 5 ++-- .../termgenerator/SuperTermGenerator.java | 3 +- .../TestApplyUpdateOnRigidCondition.java | 3 +- .../logic/TerminalSyntaxElement.java | 5 +++- 75 files changed, 224 insertions(+), 182 deletions(-) delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/op/SVSubstitute.java 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/JavaNonTerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java index 4f1dfdb2ff2..ded5c975478 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,7 +5,6 @@ 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; 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 d9709324c9d..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,6 @@ 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; @@ -14,7 +13,7 @@ * to achieve an immutable structure */ -public interface SourceElement extends SVSubstitute, SyntaxElement { +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 d240ddafb2e..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,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java; -import org.key_project.logic.SyntaxElement; import org.key_project.logic.TerminalSyntaxElement; /** 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 c6533ebfe38..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,7 +4,6 @@ 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; 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 f99f1494181..6efc4cf1f20 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,7 +5,6 @@ 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/ILoopInit.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java index 362b5b85e4a..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 @@ -5,7 +5,6 @@ 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; 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 6457646b443..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 @@ -17,6 +17,7 @@ import de.uka.ilkd.key.java.statement.ILoopInit; import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.logic.op.IProgramVariable; + import org.key_project.logic.SyntaxElement; /** @@ -31,5 +32,5 @@ public interface ProgramConstruct extends Expression, Statement, ILoopInit, IFor SyntaxElement getChild(int n); @Override - int getChildCount() ; + 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/TermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java index a1ffadb28ea..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 @@ -152,7 +152,7 @@ * @see TermLabelManager */ // spotless:on -public interface TermLabel extends Named, SyntaxElement, /* TODO: Remove*/ TerminalSyntaxElement { +public interface TermLabel extends Named, SyntaxElement, /* TODO: Remove */ TerminalSyntaxElement { /** * Retrieves the i-th parameter object of this term label. 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/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 efd705956fc..394c0f736a1 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 @@ -23,7 +23,6 @@ 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; @@ -34,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 , SyntaxElement { +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 = 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 ed06827732d..2450b036d2e 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 @@ -5,7 +5,6 @@ import java.util.WeakHashMap; -import org.key_project.logic.SyntaxElement; import org.key_project.logic.TerminalSyntaxElement; public class Qualifier implements TerminalSyntaxElement { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SVSubstitute.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SVSubstitute.java deleted file mode 100644 index b7f183d6ed5..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SVSubstitute.java +++ /dev/null @@ -1,12 +0,0 @@ -/* 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; - -/** - * JavaCardDL syntactical elements implement this interface if they can occur as instantiations of - * schema variables. - */ -public interface SVSubstitute { - -} 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 bb21080c5a3..4ca7e30a52f 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,13 +6,15 @@ 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, /*TODO: check*/ TerminalSyntaxElement { +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/VariableSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/VariableSV.java index 732769c23b4..fcbec1e7937 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 @@ -12,7 +12,8 @@ /** * Schema variable that is instantiated with logical variables. */ -public final class VariableSV extends OperatorSV implements QuantifiableVariable, TerminalSyntaxElement { +public final class VariableSV extends OperatorSV + implements QuantifiableVariable, TerminalSyntaxElement { /** * Creates a new SchemaVariable that is used as placeholder for bound(quantified) variables. diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java index 55a54a489f3..a50e7a424b1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java @@ -10,9 +10,9 @@ import de.uka.ilkd.key.logic.TermFactory; 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 de.uka.ilkd.key.util.InfFlowSpec; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -36,7 +36,7 @@ public class OpReplacer { /** * The replacement map. */ - private final ReplacementMap map; + private final ReplacementMap map; /** *

@@ -53,7 +53,7 @@ public class OpReplacer { * with * @param tf a term factory. */ - public OpReplacer(Map map, TermFactory tf) { + public OpReplacer(Map map, TermFactory tf) { this(map, tf, null); } @@ -65,12 +65,12 @@ public OpReplacer(Map map, TermF * @param tf a term factory. * @param proof the currently loaded proof */ - public OpReplacer(Map map, TermFactory tf, + public OpReplacer(Map map, TermFactory tf, Proof proof) { assert map != null; this.map = map instanceof ReplacementMap - ? (ReplacementMap) map + ? (ReplacementMap) map : ReplacementMap.create(tf, proof, map); this.tf = tf; @@ -234,7 +234,7 @@ public Term replace(Term term) { return newTerm; } - for (SVSubstitute svs : map.keySet()) { + for (SyntaxElement svs : map.keySet()) { if (term.equalsModProperty(svs, TERM_LABELS_PROPERTY)) { return (Term) map.get(svs); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java index 88fe0af0499..a6df47649fb 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java @@ -11,11 +11,12 @@ import de.uka.ilkd.key.logic.TermFactory; import de.uka.ilkd.key.logic.label.OriginTermLabel; import de.uka.ilkd.key.logic.label.TermLabelManager; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.settings.TermLabelSettings; import de.uka.ilkd.key.util.LinkedHashMap; +import org.key_project.logic.SyntaxElement; + /** * A map to be used in an {@link OpReplacer}. It maps operators that should be replaced to their * replacements. @@ -25,7 +26,7 @@ * @param the type of the elements to replace. * @param the type of the replacements. */ -public interface ReplacementMap extends Map { +public interface ReplacementMap extends Map { /** * Creates a new replacement map. @@ -36,7 +37,7 @@ public interface ReplacementMap extends Map { * @param proof the currently loaded proof, or {@code null} if no proof is loaded. * @return a new replacement map. */ - static ReplacementMap create(TermFactory tf, + static ReplacementMap create(TermFactory tf, Proof proof) { var noIrrelevantTermLabelsMap = proof == null ? ProofSettings.DEFAULT_SETTINGS.getTermLabelSettings().getUseOriginLabels() @@ -58,7 +59,7 @@ static ReplacementMap create(TermFactory tf, * @param initialMappings a map whose mapping should be added to the new replacement map. * @return a new replacement map. */ - static ReplacementMap create(TermFactory tf, + static ReplacementMap create(TermFactory tf, Proof proof, Map initialMappings) { ReplacementMap result = create(tf, proof); result.putAll(initialMappings); @@ -77,7 +78,7 @@ static ReplacementMap create(TermFactory tf, * @param the type of the operators to replace. * @param the type of the replacements. */ - class DefaultReplacementMap extends LinkedHashMap + class DefaultReplacementMap extends LinkedHashMap implements ReplacementMap { private static final long serialVersionUID = 6223486569442129676L; } @@ -98,7 +99,7 @@ class DefaultReplacementMap extends LinkedHashMap + class NoIrrelevantLabelsReplacementMap implements ReplacementMap { /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java index 567b38b68f1..9ca5be95b01 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java @@ -6,9 +6,10 @@ import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; +import org.key_project.logic.SyntaxElement; + public interface TacletMatcher { /** @@ -69,7 +70,7 @@ MatchConditions checkConditions(MatchConditions p_matchconditions, * instantiationCandidate or null if a match was not possible */ MatchConditions checkVariableConditions(SchemaVariable var, - SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services); + SyntaxElement instantiationCandidate, MatchConditions matchCond, Services services); /** * matches the given term against the taclet's find term if the taclet has no find term or the diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableCondition.java index aa9cc4495e5..1907547ddc7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableCondition.java @@ -4,9 +4,10 @@ package de.uka.ilkd.key.rule; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; +import org.key_project.logic.SyntaxElement; + /** * The instantiations of a schemavariable can be restricted on rule scope by attaching conditions on @@ -30,7 +31,8 @@ public interface VariableCondition { * @return modified match results if the condition can be satisfied, or null * otherwise */ - MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions matchCond, + MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, + MatchConditions matchCond, Services services); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java index cb29e713636..d2c19ec07fb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java @@ -4,10 +4,11 @@ package de.uka.ilkd.key.rule; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * The variable condition adapter can be used by variable conditions which can either fail or be @@ -24,13 +25,13 @@ public abstract class VariableConditionAdapter implements VariableCondition { * @param services the program information object * @return true iff condition is fulfilled */ - public abstract boolean check(SchemaVariable var, SVSubstitute instCandidate, + public abstract boolean check(SchemaVariable var, SyntaxElement instCandidate, SVInstantiations instMap, Services services); @Override - public final MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, + public final MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, MatchConditions mc, Services services) { return check(var, instCandidate, mc.getInstantiations(), services) ? mc : null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java index 396d872b368..8ff2d7edcb0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java @@ -4,11 +4,11 @@ package de.uka.ilkd.key.rule.conditions; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; @@ -34,7 +34,7 @@ public TypeResolver getTypeResolver() { } @Override - public boolean check(SchemaVariable var, SVSubstitute instCandidate, SVInstantiations instMap, + public boolean check(SchemaVariable var, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { final Sort sort = resolver.resolveSort(var, instCandidate, instMap, services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java index 5ac5d19f8b3..8b1455e32bb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java @@ -5,11 +5,12 @@ import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * disjoin two variable conditions @@ -30,7 +31,7 @@ public AlternativeVariableCondition(VariableConditionAdapter delegate0, * check whether any of the two delegates apply */ @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { return delegate0.check(var, subst, svInst, services) || delegate1.check(var, subst, svInst, services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java index 78f40a82ba6..511ce913b22 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.rule.inst.SVInstantiations; 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.ImmutableSet; @@ -198,7 +199,8 @@ private static boolean nameIsAlreadyUsed(Name name, ImmutableSet toExpArray( @SuppressWarnings("unchecked") @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { Map tacletOptions = services.getProof().getSettings().getChoiceSettings().getDefaultChoices(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java index 58f2f5e8ef4..a657c581069 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java @@ -10,6 +10,7 @@ import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.Function; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; @@ -66,7 +67,7 @@ private static boolean clearlyDisjoint(Term t1, Term t2, Services services) { @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { final Term s1Inst = (Term) svInst.getInstantiation(var1); final Term s2Inst = (Term) svInst.getInstantiation(var2); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java index 84b479a3a64..cfcc8aa1240 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java @@ -20,11 +20,12 @@ import de.uka.ilkd.key.java.reference.FieldReference; import de.uka.ilkd.key.logic.op.ProgramConstant; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * This variable condition checks if the instantiation of a schemavariable (of * type Field) refers to a Java field declared as "model". @@ -47,7 +48,7 @@ public ModelFieldCondition(SchemaVariable field, boolean negated) { } @Override - public boolean check(SchemaVariable var, SVSubstitute subst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations instMap, Services services) { if (var == field) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java index 063b580d813..4823f007a09 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java @@ -12,7 +12,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.visitor.LabelCollector; import de.uka.ilkd.key.logic.op.ProgramSV; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.ProgramSVSort; import de.uka.ilkd.key.rule.MatchConditions; @@ -20,6 +19,7 @@ import de.uka.ilkd.key.rule.inst.InstantiationEntry; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableMapEntry; /** @@ -41,11 +41,11 @@ public NewJumpLabelCondition(SchemaVariable sv) { } @Override - public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, + public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, MatchConditions matchCond, Services services) { if (var != labelSV && matchCond.getInstantiations().isInstantiated(labelSV)) { var = labelSV; - instCandidate = (SVSubstitute) matchCond.getInstantiations().getInstantiation(labelSV); + instCandidate = (SyntaxElement) matchCond.getInstantiations().getInstantiation(labelSV); } if (var == labelSV) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java index 88695c74bd0..8c877c2cc6c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java @@ -7,13 +7,14 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.IObserverFunction; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.TermSV; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.VariableCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + public final class ObserverCondition implements VariableCondition { @@ -28,7 +29,8 @@ public ObserverCondition(TermSV obs, TermSV heap) { @Override - public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, + public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, + MatchConditions mc, Services services) { SVInstantiations svInst = mc.getInstantiations(); final Term obsInst = (Term) svInst.getInstantiation(obs); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java index 52287cf0a6f..2249534b53e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.IObserverFunction; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.UseDependencyContractRule; @@ -17,6 +16,7 @@ import de.uka.ilkd.key.speclang.Contract; import org.key_project.logic.ParsableVariable; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableSet; /** @@ -70,7 +70,8 @@ public SameObserverCondition(ParsableVariable schema1, ParsableVariable schema2) // explanation see class javadoc. @Override - public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, + public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, + MatchConditions mc, Services services) { SVInstantiations svInst = mc.getInstantiations(); final Term term1 = (Term) svInst.getInstantiation(schema1); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java index 980911205ec..7b64f04a5c5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java @@ -17,6 +17,7 @@ import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.Named; +import org.key_project.logic.SyntaxElement; public class SimplifyIfThenElseUpdateCondition implements VariableCondition { @@ -151,7 +152,8 @@ private Term simplify(Term phi, Term u1, Term u2, Term t, TermServices services) @Override - public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, + public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, + MatchConditions mc, Services services) { SVInstantiations svInst = mc.getInstantiations(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java index 2d942802bf8..f850a1d42be 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java @@ -10,6 +10,8 @@ import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * This variable condition checks if the instantiation of a schemavariable (of type Field) refers to * a Java field declared as "static". @@ -31,7 +33,7 @@ public StaticFieldCondition(SchemaVariable field, boolean negated) { } @Override - public boolean check(SchemaVariable var, SVSubstitute instCandidate, SVInstantiations instMap, + public boolean check(SchemaVariable var, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { final Object o = instMap.getInstantiation(field); if (!(o instanceof Term f)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticMethodCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticMethodCondition.java index 2ce44dab8b6..10524eba651 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticMethodCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticMethodCondition.java @@ -13,12 +13,12 @@ import de.uka.ilkd.key.java.reference.ReferencePrefix; import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.NullSort; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableArray; @@ -58,7 +58,7 @@ private static ImmutableArray toExpArray( @SuppressWarnings("unchecked") @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { ReferencePrefix rp = (ReferencePrefix) svInst.getInstantiation(caller); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticReferenceCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticReferenceCondition.java index c3ce83b2aa2..332bba35df2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticReferenceCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticReferenceCondition.java @@ -8,11 +8,12 @@ import de.uka.ilkd.key.java.reference.FieldReference; import de.uka.ilkd.key.logic.op.ProgramConstant; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * ensures that the given instantiation for the schemavariable denotes a static field @@ -34,7 +35,7 @@ public StaticReferenceCondition(SchemaVariable reference, boolean negation) { @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { if (var == reference) { 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 74f87909a8f..a92a20bdb21 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 @@ -9,13 +9,14 @@ import de.uka.ilkd.key.logic.JavaBlock; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.ProgramSV; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.LightweightSyntacticalReplaceVisitor; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.VariableCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * Stores the given {@link Statement}, after substitution of {@link SchemaVariable}s, into the given * {@link ProgramSV} for later use in other conditions and transformers. The arguments are a @@ -37,7 +38,7 @@ public StoreStmtInCondition(ProgramSV resultVarSV, Term term) { } @Override - public MatchConditions check(SchemaVariable sv, SVSubstitute instCandidate, + public MatchConditions check(SchemaVariable sv, SyntaxElement instCandidate, MatchConditions matchCond, Services services) { final SVInstantiations svInst = matchCond.getInstantiations(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java index a155d62dc1c..6b6e31e5b4e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java @@ -5,13 +5,14 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.LightweightSyntacticalReplaceVisitor; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.VariableCondition; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * Stores the given {@link Term}, after substitution of {@link SchemaVariable}s, into the given * {@link SchemaVariable} for later use in other conditions and transformers. @@ -28,7 +29,7 @@ public StoreTermInCondition(SchemaVariable resultVarSV, Term term) { } @Override - public MatchConditions check(SchemaVariable sv, SVSubstitute instCandidate, + public MatchConditions check(SchemaVariable sv, SyntaxElement instCandidate, MatchConditions matchCond, Services services) { final SVInstantiations svInst = matchCond.getInstantiations(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java index 7787df797dd..2ac0c4428a2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java @@ -7,11 +7,12 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.FormulaSV; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; + /** * This variable condition checks if an instantiation for a formula has sub formulas which are * formulas. It returns false for an arity equal to zero or no sub formulas. This is needed to @@ -32,7 +33,7 @@ public SubFormulaCondition(FormulaSV a, boolean negated) { } @Override - public boolean check(SchemaVariable var, SVSubstitute instCandidate, SVInstantiations instMap, + public boolean check(SchemaVariable var, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { if (!(var instanceof FormulaSV) || var != this.a) { return false; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java index 1f29050176e..6bccef558d5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java @@ -5,13 +5,13 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.TermLabelSV; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableArray; /** @@ -33,7 +33,7 @@ public TermLabelCondition(TermLabelSV l, String t, boolean negated) { } @Override - public boolean check(SchemaVariable var, SVSubstitute instCandidate, SVInstantiations instMap, + public boolean check(SchemaVariable var, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { assert instMap.getInstantiation(l) instanceof ImmutableArray; ImmutableArray tInsts = (ImmutableArray) instMap.getInstantiation(l); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java index 6d49717e70d..3c28d087433 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java @@ -12,7 +12,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.java.declaration.InterfaceDeclaration; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.ArraySort; import de.uka.ilkd.key.logic.sort.NullSort; @@ -20,6 +19,7 @@ import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; @@ -72,7 +72,7 @@ public Mode getMode() { } @Override - public boolean check(SchemaVariable var, SVSubstitute subst, SVInstantiations svInst, + public boolean check(SchemaVariable var, SyntaxElement subst, SVInstantiations svInst, Services services) { if (!fst.isComplete(var, subst, svInst, services) diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeCondition.java index febb37096b7..7f041a3731a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeCondition.java @@ -5,13 +5,13 @@ import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.NullSort; import de.uka.ilkd.key.logic.sort.ProxySort; import de.uka.ilkd.key.rule.VariableConditionAdapter; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; @@ -55,7 +55,7 @@ public boolean getNonNull() { @Override - public boolean check(SchemaVariable p_var, SVSubstitute candidate, SVInstantiations svInst, + public boolean check(SchemaVariable p_var, SyntaxElement candidate, SVInstantiations svInst, Services services) { if (!resolver.isComplete(p_var, candidate, svInst, services)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java index f7dd7617ab8..f313becfd78 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java @@ -11,13 +11,13 @@ import de.uka.ilkd.key.logic.op.IObserverFunction; import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.util.Debug; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.Function; import org.key_project.logic.sort.Sort; @@ -50,10 +50,10 @@ public static TypeResolver createNonGenericSortResolver(Sort s) { } - public abstract boolean isComplete(SchemaVariable sv, SVSubstitute instCandidate, + public abstract boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services); - public abstract Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, + public abstract Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services); @@ -74,13 +74,13 @@ public GenericSort getGenericSort() { } @Override - public boolean isComplete(SchemaVariable sv, SVSubstitute instCandidate, + public boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services) { return instMap.getGenericSortInstantiations().getInstantiation(gs) != null; } @Override - public Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, + public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { return instMap.getGenericSortInstantiations().getInstantiation(gs); } @@ -100,13 +100,13 @@ public NonGenericSortResolver(Sort s) { } @Override - public boolean isComplete(SchemaVariable sv, SVSubstitute instCandidate, + public boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services) { return true; } @Override - public Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, + public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { return s; } @@ -130,18 +130,18 @@ public ElementTypeResolverForSV(SchemaVariable sv) { } @Override - public boolean isComplete(SchemaVariable sv, SVSubstitute instCandidate, + public boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services) { return resolveSV == sv || instMap.getInstantiation(resolveSV) != null; } @Override - public Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, + public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { final Sort s; - final SVSubstitute inst = (SVSubstitute) (resolveSV == sv ? instCandidate + final SyntaxElement inst = (SyntaxElement) (resolveSV == sv ? instCandidate : instMap.getInstantiation(resolveSV)); if (inst instanceof ProgramVariable) { @@ -178,18 +178,18 @@ public ContainerTypeResolver(SchemaVariable sv) { } @Override - public boolean isComplete(SchemaVariable sv, SVSubstitute instCandidate, + public boolean isComplete(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, TermServices services) { return sv == memberSV || instMap.getInstantiation(memberSV) != null; } @Override - public Sort resolveSort(SchemaVariable sv, SVSubstitute instCandidate, + public Sort resolveSort(SchemaVariable sv, SyntaxElement instCandidate, SVInstantiations instMap, Services services) { final Sort result; - final SVSubstitute inst = (SVSubstitute) (memberSV == sv ? instCandidate + final SyntaxElement inst = (SyntaxElement) (memberSV == sv ? instCandidate : instMap.getInstantiation(memberSV)); if (inst instanceof Operator) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramList.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramList.java index 408e0b82b92..e5f38ccbc06 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramList.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramList.java @@ -4,11 +4,11 @@ package de.uka.ilkd.key.rule.inst; import de.uka.ilkd.key.java.ProgramElement; -import de.uka.ilkd.key.logic.op.SVSubstitute; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableArray; -public class ProgramList implements SVSubstitute { +public class ProgramList implements SyntaxElement { private final ImmutableArray list; @@ -34,4 +34,14 @@ public int hashCode() { return list.hashCode(); } + + @Override + public SyntaxElement getChild(int n) { + return list.get(n); + } + + @Override + public int getChildCount() { + return list.size(); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java index ef2d5270d82..7832eae3b67 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java @@ -13,7 +13,6 @@ import de.uka.ilkd.key.logic.Term; 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 de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.UpdateApplication; import de.uka.ilkd.key.rule.FindTaclet; @@ -30,6 +29,7 @@ import de.uka.ilkd.key.rule.match.TacletMatcherKit; import de.uka.ilkd.key.rule.match.vm.instructions.MatchSchemaVariableInstruction; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; @@ -239,8 +239,8 @@ public final MatchConditions checkConditions(MatchConditions cond, Services serv while (result != null && svIterator.hasNext()) { final SchemaVariable sv = svIterator.next(); final Object o = result.getInstantiations().getInstantiation(sv); - if (o instanceof SVSubstitute) { - result = checkVariableConditions(sv, (SVSubstitute) o, result, services); + if (o instanceof SyntaxElement) { + result = checkVariableConditions(sv, (SyntaxElement) o, result, services); } } } @@ -279,7 +279,7 @@ private boolean varIsBound(SchemaVariable v) { */ @Override public final MatchConditions checkVariableConditions(SchemaVariable var, - SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services) { + SyntaxElement instantiationCandidate, MatchConditions matchCond, Services services) { if (matchCond != null) { if (instantiationCandidate instanceof Term term) { if (!(term.op() instanceof QuantifiableVariable)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java index 2ddd6dbc086..ccca2629fd4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java @@ -14,7 +14,6 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.IObserverFunction; import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.proof.OpReplacer; import de.uka.ilkd.key.proof.init.ContractPO; @@ -22,6 +21,7 @@ import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.ProofOblInput; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableList; import org.key_project.util.java.MapUtil; @@ -145,7 +145,7 @@ public Term getPre(LocationVariable heap, LocationVariable selfVar, assert paramVars != null; assert paramVars.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); if (originalSelfVar != null) { map.put(originalSelfVar, selfVar); } @@ -192,7 +192,7 @@ public Term getPre(LocationVariable heap, Term heapTerm, Term selfTerm, assert paramTerms != null; assert paramTerms.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); map.put(services.getTermBuilder().var(heap), heapTerm); if (originalSelfVar != null) { map.put(services.getTermBuilder().var(originalSelfVar), selfTerm); @@ -259,7 +259,7 @@ public Term getMby(LocationVariable selfVar, ImmutableList par assert paramVars != null; assert paramVars.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); if (originalSelfVar != null) { map.put(originalSelfVar, selfVar); } @@ -281,7 +281,7 @@ public Term getMby(Map heapTerms, Term selfTerm, assert paramTerms != null; assert paramTerms.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); for (LocationVariable heap : heapTerms.keySet()) { map.put(services.getTermBuilder().var(heap), heapTerms.get(heap)); } @@ -370,7 +370,7 @@ public Term getDep(LocationVariable heap, boolean atPre, LocationVariable selfVa assert paramVars != null; assert paramVars.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); if (originalSelfVar != null) { map.put(originalSelfVar, selfVar); } @@ -400,7 +400,7 @@ public Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term sel assert paramTerms != null; assert paramTerms.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); map.put(services.getTermBuilder().var(heap), heapTerm); if (originalSelfVar != null) { map.put(services.getTermBuilder().var(originalSelfVar), selfTerm); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java index 6023d0880c5..48125b113a3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java @@ -29,6 +29,7 @@ import de.uka.ilkd.key.proof.init.ProofOblInput; import org.key_project.logic.Named; +import org.key_project.logic.SyntaxElement; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -741,7 +742,7 @@ public static String getText(FunctionalOperationContract contract, private static String getSignatureText(IProgramMethod pm, Operator originalResultVar, - Operator originalSelfVar, ImmutableList originalParamVars, + Operator originalSelfVar, ImmutableList originalParamVars, LocationVariable originalExcVar, Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols) { final StringBuilder sig = new StringBuilder(); @@ -758,7 +759,7 @@ private static String getSignatureText(IProgramMethod pm, Operator originalResul } sig.append(pm.getName()); sig.append("("); - for (SVSubstitute subst : originalParamVars) { + for (SyntaxElement subst : originalParamVars) { if (subst instanceof Named named) { sig.append(named.name()).append(", "); } else if (subst instanceof Term) { @@ -863,7 +864,7 @@ private static String getPostText(Map originalPosts, } private static String getText(IProgramMethod pm, Operator originalResultVar, - Operator originalSelfVar, ImmutableList originalParamVars, + Operator originalSelfVar, ImmutableList originalParamVars, LocationVariable originalExcVar, boolean hasMby, Term originalMby, Map originalMods, Map hasRealModifiesClause, Term globalDefs, @@ -1288,7 +1289,7 @@ public Term getDep(LocationVariable heap, boolean atPre, LocationVariable selfVa assert paramVars != null; assert paramVars.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); if (originalSelfVar != null) { map.put(originalSelfVar, selfVar); } @@ -1316,7 +1317,7 @@ public Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term sel assert paramTerms != null; assert paramTerms.size() == originalParamVars.size(); assert services != null; - Map map = new LinkedHashMap<>(); + Map map = new LinkedHashMap<>(); map.put(tb.var(heap), heapTerm); if (originalSelfVar != null) { map.put(tb.var(originalSelfVar), selfTerm); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java index a4cee8a6683..13c702544ae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java @@ -41,13 +41,13 @@ import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.Modality; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; import de.uka.ilkd.key.proof.OpReplacer; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination; import de.uka.ilkd.key.speclang.jml.pretranslation.Behavior; import de.uka.ilkd.key.util.InfFlowSpec; +import org.key_project.logic.SyntaxElement; import org.key_project.util.ExtList; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; @@ -329,7 +329,7 @@ public static LoopContract combine(ImmutableSet contracts, Service */ private static OpReplacer createOpReplacer(final ProgramVariable index, final ProgramVariable values, Services services) { - final Map replacementMap = new HashMap<>(); + final Map replacementMap = new HashMap<>(); if (index != null) { replacementMap.put(services.getTermBuilder().index(), services.getTermBuilder().var(index)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/ReplacementMap.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/ReplacementMap.java index 0e1617da870..3bfcaf07435 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/ReplacementMap.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/ReplacementMap.java @@ -13,7 +13,8 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; -import de.uka.ilkd.key.logic.op.SVSubstitute; + +import org.key_project.logic.SyntaxElement; /** * A map from some type to the same type. @@ -22,7 +23,7 @@ * * @author lanzinger */ -public abstract class ReplacementMap +public abstract class ReplacementMap extends de.uka.ilkd.key.proof.ReplacementMap.NoIrrelevantLabelsReplacementMap { /** 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 201090e5703..49368cb1602 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 @@ -96,7 +96,8 @@ protected Term generateOneTerm(Term superterm, int child) { return services.getTermBuilder().tf().createTerm(binFunc, superterm, index); } - private static class SuperTermGeneratedOp implements SortedOperator, Operator, TerminalSyntaxElement { + 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/rule/conditions/TestApplyUpdateOnRigidCondition.java b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java index 91ff2692110..fae51cc5a3e 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java @@ -12,6 +12,7 @@ import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.sort.Sort; import org.junit.jupiter.api.Test; @@ -229,7 +230,7 @@ private Term applyUpdateOnTerm(Term term) { * @param tOrPhi the {@link SchemaVariable} that is instantiated with the term or formula in * term * @param result the {@link SchemaVariable} that is instantiated with the result of a - * {@link ApplyUpdateOnRigidCondition#check(SchemaVariable, SVSubstitute, MatchConditions, Services)} + * {@link ApplyUpdateOnRigidCondition#check(SchemaVariable, SyntaxElement, MatchConditions, Services)} * call * * @return the original formula or term if the update cannot be applied; else, the updated 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 index e6d25f7ae00..860f1e62a65 100644 --- a/key.ncore/src/main/java/org/key_project/logic/TerminalSyntaxElement.java +++ b/key.ncore/src/main/java/org/key_project/logic/TerminalSyntaxElement.java @@ -1,6 +1,9 @@ +/* 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 org.key_project.logic; -public interface TerminalSyntaxElement extends SyntaxElement{ +public interface TerminalSyntaxElement extends SyntaxElement { @Override default SyntaxElement getChild(int n) { throw new IndexOutOfBoundsException(this.getClass() + " " + this + " has no children");