Minor code cleanup

Add missing @OverRide annotations
Drodt · Jan 31, 2025 · be361cb · be361cb
1 parent 619275a
commit be361cb
Show file tree

Hide file tree

Showing 45 changed files with 117 additions and 2 deletions.
diff --git a/.../src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionStrategy.java b/.../src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionStrategy.java
@@ -111,7 +111,7 @@ protected Feature setupApprovalF() {
         // Make sure that cuts are only applied if the cut term is not already part of the sequent.
         // This check is performed exactly before the rule is applied because the sequent might has
         // changed in the time after the schema variable instantiation was instantiated.
-        SetRuleFilter depFilter = new SetRuleFilter();
+        final SetRuleFilter depFilter = new SetRuleFilter();
         depFilter.addRuleToSet(getProof().getInitConfig().lookupActiveTaclet(new Name("cut")));
         result = add(result,
             ConditionalFeature.createConditional(depFilter, new CutHeapObjectsFeature()));

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/AbstractFeatureStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/AbstractFeatureStrategy.java
@@ -111,6 +111,7 @@ protected void clearRuleSetBindings(RuleSetDispatchFeature d, String ruleSet) {
     }
 
 
+    @Override
     public void instantiateApp(RuleApp app, PosInOccurrence pio,
             Goal goal,
             RuleAppCostCollector collector) {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FIFOStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FIFOStrategy.java
@@ -49,25 +49,30 @@ private FIFOStrategy() {
      *
      * @return true iff the rule should be applied, false otherwise
      */
+    @Override
     public boolean isApprovedApp(RuleApp app, PosInOccurrence pio,
             Goal goal) {
         return true;
     }
 
+    @Override
     public void instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal,
             RuleAppCostCollector collector) {}
 
+    @Override
     public Name name() {
         return NAME;
     }
 
     public static final Strategy INSTANCE = new FIFOStrategy();
 
     public static class Factory implements StrategyFactory {
+        @Override
         public Name name() {
             return NAME;
         }
 
+        @Override
         public Strategy create(Proof proof, StrategyProperties properties) {
             return INSTANCE;
         }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java
@@ -1442,12 +1442,15 @@ private void setupInEqSimp(RuleSetDispatchFeature d, IntegerLDT numbers) {
 
         final Term tOne = getServices().getTermBuilder().zTerm("1");
         final TermBuffer one = new TermBuffer() {
+            @Override
             public void setContent(org.key_project.logic.Term term, MutableState mState) {}
 
+            @Override
             public Term getContent(MutableState mState) {
                 return tOne;
             }
 
+            @Override
             public Term toTerm(RuleApp app, PosInOccurrence pos,
                     Goal goal, MutableState mState) {
                 return tOne;
@@ -1456,12 +1459,15 @@ public Term toTerm(RuleApp app, PosInOccurrence pos,
 
         final Term tTwo = getServices().getTermBuilder().zTerm("2");
         final TermBuffer two = new TermBuffer() {
+            @Override
             public void setContent(org.key_project.logic.Term term, MutableState mState) {}
 
+            @Override
             public Term getContent(MutableState mState) {
                 return tTwo;
             }
 
+            @Override
             public Term toTerm(RuleApp app, PosInOccurrence pos,
                     Goal goal, MutableState mState) {
                 return tTwo;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategyFactory.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategyFactory.java
@@ -450,6 +450,7 @@ private static OneOfStrategyPropertyDefinition getUserOptions() {
             -1, props.toArray(new AbstractStrategyPropertyDefinition[0]));
     }
 
+    @Override
     public Strategy create(Proof proof, StrategyProperties strategyProperties) {
         return new JavaCardDLStrategy(proof, strategyProperties);
     }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SimpleFilteredStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SimpleFilteredStrategy.java
@@ -40,6 +40,7 @@ public SimpleFilteredStrategy(RuleFilter p_ruleFilter) {
         ruleFilter = p_ruleFilter;
     }
 
+    @Override
     public Name name() {
         return NAME;
     }
@@ -79,13 +80,15 @@ public Name name() {
      *
      * @return true iff the rule should be applied, false otherwise
      */
+    @Override
     public boolean isApprovedApp(RuleApp app, PosInOccurrence pio,
             Goal goal) {
         // do not apply a rule twice
         return !(app instanceof TacletApp) || NonDuplicateAppFeature.INSTANCE.computeCost(app, pio,
             goal, new MutableState()) != TopRuleAppCost.INSTANCE;
     }
 
+    @Override
     public void instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal,
             RuleAppCostCollector collector) {}
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java
@@ -395,6 +395,7 @@ public void write(Configuration category) {
     }
 
 
+    @Override
     public String getProperty(String key) {
         String val = super.getProperty(key);
         if (val != null) {
@@ -436,6 +437,7 @@ public void write(Properties p) {
     }
 
 
+    @Override
     public synchronized Object clone() {
         final Properties p = (Properties) super.clone();
         final StrategyProperties sp = new StrategyProperties();

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractBetaFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractBetaFeature.java
@@ -98,6 +98,7 @@ public int compute(Term p_t, boolean p_positive) {
     }
 
     private static class MaxPosPathHelper extends MaxPathHelper {
+        @Override
         protected int computeDefault(Term p_t, boolean p_positive) {
             if (alwaysReplace(p_t)) {
                 return 1;
@@ -108,6 +109,7 @@ protected int computeDefault(Term p_t, boolean p_positive) {
     }
 
     private static class MaxDPathHelper extends MaxPathHelper {
+        @Override
         protected int computeDefault(Term p_t, boolean p_positive) {
             return 1;
         }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AtomsSmallerThanFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AtomsSmallerThanFeature.java
@@ -38,6 +38,7 @@ public static Feature create(ProjectionToTerm<Goal> left, ProjectionToTerm<Goal>
         return new AtomsSmallerThanFeature(left, right, numbers);
     }
 
+    @Override
     protected boolean filter(TacletApp app, PosInOccurrence pos,
             Goal goal, MutableState mState) {
         return lessThan(collectAtoms(left.toTerm(app, pos, goal, mState)),

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java
@@ -26,6 +26,7 @@ public class CheckApplyEqFeature extends BinaryTacletAppFeature {
 
     private CheckApplyEqFeature() {}
 
+    @Override
     protected boolean filter(TacletApp p_app, PosInOccurrence pos, Goal goal, MutableState mState) {
         assert pos != null : "Need to know the position of " + "the application of the taclet";
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/EqNonDuplicateAppFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/EqNonDuplicateAppFeature.java
@@ -23,6 +23,7 @@ public class EqNonDuplicateAppFeature extends AbstractNonDuplicateAppFeature {
 
     private EqNonDuplicateAppFeature() {}
 
+    @Override
     public boolean filter(TacletApp app, PosInOccurrence pos,
             Goal goal, MutableState mState) {
         assert pos != null : "Feature is only applicable to rules with find";
@@ -34,6 +35,7 @@ public boolean filter(TacletApp app, PosInOccurrence pos,
         return noDuplicateFindTaclet(app, pos, goal);
     }
 
+    @Override
     protected boolean comparePio(TacletApp newApp, TacletApp oldApp,
             PosInOccurrence newPio,
             PosInOccurrence oldPio) {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ImplicitCastNecessary.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ImplicitCastNecessary.java
@@ -24,6 +24,7 @@ private ImplicitCastNecessary(ProjectionToTerm<Goal> projection) {
         this.projection = projection;
     }
 
+    @Override
     protected <G extends ProofGoal<@NonNull G>> boolean filter(RuleApp app, PosInOccurrence pos,
             G goal, MutableState mState) {
         assert pos != null && pos.depth() >= 1;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InEquationMultFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InEquationMultFeature.java
@@ -37,6 +37,7 @@ public abstract class InEquationMultFeature extends BinaryTacletAppFeature {
     public static Feature partiallyBounded(ProjectionToTerm<Goal> mult1Candidate,
             ProjectionToTerm<Goal> mult2Candidate, ProjectionToTerm<Goal> targetCandidate) {
         return new InEquationMultFeature(mult1Candidate, mult2Candidate, targetCandidate) {
+            @Override
             protected boolean filter(Monomial targetM, Monomial mult1M, Monomial mult2M) {
                 return !mult2M.reduce(targetM).variablesDisjoint(mult1M)
                         && !mult1M.reduce(targetM).variablesDisjoint(mult2M);
@@ -50,6 +51,7 @@ protected boolean filter(Monomial targetM, Monomial mult1M, Monomial mult2M) {
     public static Feature totallyBounded(ProjectionToTerm<Goal> mult1Candidate,
             ProjectionToTerm<Goal> mult2Candidate, ProjectionToTerm<Goal> targetCandidate) {
         return new InEquationMultFeature(mult1Candidate, mult2Candidate, targetCandidate) {
+            @Override
             protected boolean filter(Monomial targetM, Monomial mult1M, Monomial mult2M) {
                 return targetM.variablesSubsume(mult1M.multiply(mult2M));
             }
@@ -62,6 +64,7 @@ protected boolean filter(Monomial targetM, Monomial mult1M, Monomial mult2M) {
     public static Feature exactlyBounded(ProjectionToTerm<Goal> mult1Candidate,
             ProjectionToTerm<Goal> mult2Candidate, ProjectionToTerm<Goal> targetCandidate) {
         return new InEquationMultFeature(mult1Candidate, mult2Candidate, targetCandidate) {
+            @Override
             protected boolean filter(Monomial targetM, Monomial mult1M, Monomial mult2M) {
                 return targetM.variablesEqual(mult1M.multiply(mult2M));
             }
@@ -75,6 +78,7 @@ protected InEquationMultFeature(ProjectionToTerm<Goal> mult1Candidate,
         this.targetCandidate = targetCandidate;
     }
 
+    @Override
     protected final boolean filter(TacletApp app, PosInOccurrence pos, Goal goal,
             MutableState mState) {
         final Services services = goal.proof().getServices();

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InstantiatedSVFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InstantiatedSVFeature.java
@@ -29,6 +29,7 @@ protected InstantiatedSVFeature(Name svName) {
         instProj = SVInstantiationProjection.create(svName, false);
     }
 
+    @Override
     protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
         return instProj.toTerm(app, pos, goal, mState) != null;
     }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MatchedAssumesFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MatchedAssumesFeature.java
@@ -20,6 +20,7 @@ public final class MatchedAssumesFeature extends BinaryTacletAppFeature {
 
     private MatchedAssumesFeature() {}
 
+    @Override
     protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
         return app.assumesInstantionsComplete();
     }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppFeature.java
@@ -18,6 +18,7 @@ public class NonDuplicateAppFeature extends AbstractNonDuplicateAppFeature {
 
     public static final Feature INSTANCE = new NonDuplicateAppFeature();
 
+    @Override
     public boolean filter(TacletApp app, PosInOccurrence pos,
             Goal goal, MutableState mState) {
         if (!app.assumesInstantionsComplete()) {
@@ -27,6 +28,7 @@ public boolean filter(TacletApp app, PosInOccurrence pos,
         return noDuplicateFindTaclet(app, pos, goal);
     }
 
+    @Override
     protected boolean comparePio(TacletApp newApp, TacletApp oldApp,
             PosInOccurrence newPio,
             PosInOccurrence oldPio) {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/PolynomialValuesCmpFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/PolynomialValuesCmpFeature.java
@@ -41,6 +41,7 @@ public static Feature lt(ProjectionToTerm<Goal> left, ProjectionToTerm<Goal> rig
     public static Feature lt(ProjectionToTerm<Goal> left, ProjectionToTerm<Goal> right,
             ProjectionToTerm<Goal> leftCoeff, ProjectionToTerm<Goal> rightCoeff) {
         return new PolynomialValuesCmpFeature(left, right, leftCoeff, rightCoeff) {
+            @Override
             protected boolean compare(Polynomial leftPoly, Polynomial rightPoly) {
                 return leftPoly.valueLess(rightPoly);
             }
@@ -54,6 +55,7 @@ public static Feature leq(ProjectionToTerm<Goal> left, ProjectionToTerm<Goal> ri
     public static Feature leq(ProjectionToTerm<Goal> left, ProjectionToTerm<Goal> right,
             ProjectionToTerm<Goal> leftCoeff, ProjectionToTerm<Goal> rightCoeff) {
         return new PolynomialValuesCmpFeature(left, right, leftCoeff, rightCoeff) {
+            @Override
             protected boolean compare(Polynomial leftPoly, Polynomial rightPoly) {
                 return leftPoly.valueLeq(rightPoly);
             }
@@ -67,6 +69,7 @@ public static Feature eq(ProjectionToTerm<Goal> left, ProjectionToTerm<Goal> rig
     public static Feature eq(ProjectionToTerm<Goal> left, ProjectionToTerm<Goal> right,
             ProjectionToTerm<Goal> leftCoeff, ProjectionToTerm<Goal> rightCoeff) {
         return new PolynomialValuesCmpFeature(left, right, leftCoeff, rightCoeff) {
+            @Override
             protected boolean compare(Polynomial leftPoly, Polynomial rightPoly) {
                 return leftPoly.valueEq(rightPoly);
             }
@@ -80,6 +83,7 @@ public static Feature divides(ProjectionToTerm<Goal> left, ProjectionToTerm<Goal
     public static Feature divides(ProjectionToTerm<Goal> left, ProjectionToTerm<Goal> right,
             ProjectionToTerm<Goal> leftCoeff, ProjectionToTerm<Goal> rightCoeff) {
         return new PolynomialValuesCmpFeature(left, right, leftCoeff, rightCoeff) {
+            @Override
             protected boolean compare(Polynomial leftPoly, Polynomial rightPoly) {
                 // we currently only support constant polynomials
                 assert leftPoly.getParts().isEmpty();
@@ -96,6 +100,7 @@ protected boolean compare(Polynomial leftPoly, Polynomial rightPoly) {
         };
     }
 
+    @Override
     protected boolean filter(TacletApp app, PosInOccurrence pos,
             Goal goal, MutableState mState) {
         return compare(getPolynomial(left, leftCoeff, app, pos, goal, mState),

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ReducibleMonomialsFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ReducibleMonomialsFeature.java
@@ -31,6 +31,7 @@ private ReducibleMonomialsFeature(ProjectionToTerm<Goal> dividend,
     public static Feature createReducible(ProjectionToTerm<Goal> dividend,
             ProjectionToTerm<Goal> divisor) {
         return new ReducibleMonomialsFeature(dividend, divisor) {
+            @Override
             protected boolean checkReducibility(Monomial mDividend, Monomial mDivisor) {
                 return mDivisor.reducible(mDividend);
             }
@@ -40,12 +41,14 @@ protected boolean checkReducibility(Monomial mDividend, Monomial mDivisor) {
     public static Feature createDivides(ProjectionToTerm<Goal> dividend,
             ProjectionToTerm<Goal> divisor) {
         return new ReducibleMonomialsFeature(dividend, divisor) {
+            @Override
             protected boolean checkReducibility(Monomial mDividend, Monomial mDivisor) {
                 return mDivisor.divides(mDividend);
             }
         };
     }
 
+    @Override
     protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
         final Term dividendT = dividend.toTerm(app, pos, goal, mState);
         final Term divisorT = divisor.toTerm(app, pos, goal, mState);

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TermSmallerThanFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TermSmallerThanFeature.java
@@ -27,6 +27,7 @@ private TermSmallerThanFeature(ProjectionToTerm<Goal> left, ProjectionToTerm<Goa
         this.right = right;
     }
 
+    @Override
     protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
         return lessThan(left.toTerm(app, pos, goal, mState),
             right.toTerm(app, pos, goal, mState),

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ThrownExceptionFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ThrownExceptionFeature.java
@@ -67,6 +67,7 @@ private boolean blockedExceptions(Sort excType) {
         return false;
     }
 
+    @Override
     protected <Goal extends ProofGoal<@NonNull Goal>> boolean filter(RuleApp app,
             PosInOccurrence pos, Goal goal, MutableState mState) {
         return app instanceof TacletApp tacletApp

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TopLevelFindFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TopLevelFindFeature.java
@@ -21,6 +21,7 @@ public abstract class TopLevelFindFeature extends BinaryTacletAppFeature {
     private static abstract class TopLevelWithoutUpdate extends TopLevelFindFeature {
         protected abstract boolean matches(PosInOccurrence pos);
 
+        @Override
         protected boolean checkPosition(PosInOccurrence pos) {
             return pos.isTopLevel() && matches(pos);
         }
@@ -29,6 +30,7 @@ protected boolean checkPosition(PosInOccurrence pos) {
     private static abstract class TopLevelWithUpdate extends TopLevelFindFeature {
         protected abstract boolean matches(PosInOccurrence pos);
 
+        @Override
         protected boolean checkPosition(PosInOccurrence pos) {
             if (!pos.isTopLevel()) {
                 final PIOPathIterator it = pos.iterator();
@@ -44,41 +46,48 @@ protected boolean checkPosition(PosInOccurrence pos) {
     }
 
     public final static Feature ANTEC_OR_SUCC = new TopLevelWithoutUpdate() {
+        @Override
         protected boolean matches(PosInOccurrence pos) {
             return true;
         }
     };
 
     public final static Feature ANTEC = new TopLevelWithoutUpdate() {
+        @Override
         protected boolean matches(PosInOccurrence pos) {
             return pos.isInAntec();
         }
     };
 
     public final static Feature SUCC = new TopLevelWithoutUpdate() {
+        @Override
         protected boolean matches(PosInOccurrence pos) {
             return !pos.isInAntec();
         }
     };
 
     public final static Feature ANTEC_OR_SUCC_WITH_UPDATE = new TopLevelWithUpdate() {
+        @Override
         protected boolean matches(PosInOccurrence pos) {
             return true;
         }
     };
 
     public final static Feature ANTEC_WITH_UPDATE = new TopLevelWithUpdate() {
+        @Override
         protected boolean matches(PosInOccurrence pos) {
             return pos.isInAntec();
         }
     };
 
     public final static Feature SUCC_WITH_UPDATE = new TopLevelWithUpdate() {
+        @Override
         protected boolean matches(PosInOccurrence pos) {
             return !pos.isInAntec();
         }
     };
 
+    @Override
     protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
         assert pos != null : "Feature is only applicable to rules with find";
         return checkPosition(pos);

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TriggerVarInstantiatedFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TriggerVarInstantiatedFeature.java
@@ -18,6 +18,7 @@ public class TriggerVarInstantiatedFeature extends BinaryTacletAppFeature {
     private TriggerVarInstantiatedFeature() {
     }
 
+    @Override
     protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
         assert app.taclet().hasTrigger();