From 19f4f15999543cb10c1e4e7dece0471c3da8bafd Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 13 Jun 2024 09:54:23 +0200 Subject: [PATCH] spotless fixes --- .../key/rule/label/FormulaTermLabelMerger.java | 1 - .../key/rule/label/FormulaTermLabelUpdate.java | 2 +- .../rule/label/StayOnFormulaTermLabelPolicy.java | 1 - .../model/impl/ExecutionAuxiliaryContract.java | 1 - .../strategy/CutHeapObjectsFeature.java | 1 - .../strategy/SimplifyTermStrategy.java | 4 ++-- .../util/SymbolicExecutionUtil.java | 5 +++-- .../java/de/uka/ilkd/key/testgen/ProofInfo.java | 1 - .../uka/ilkd/key/testgen/TestCaseGenerator.java | 1 - .../SelfcompositionStateExpansionMacro.java | 3 ++- .../InfFlowContractAppTacletExecutor.java | 2 +- .../main/java/de/uka/ilkd/key/logic/Sequent.java | 1 - .../de/uka/ilkd/key/logic/label/TermLabel.java | 1 - .../ilkd/key/macros/AbstractBlastingMacro.java | 2 +- .../ilkd/key/proof/io/OutputStreamProofSaver.java | 3 ++- .../uka/ilkd/key/proof/join/JoinIsApplicable.java | 3 ++- .../de/uka/ilkd/key/proof/join/JoinProcessor.java | 4 ++-- .../key/proof/replay/AbstractProofReplayer.java | 2 +- .../ilkd/key/rule/AbstractBlockContractRule.java | 1 - .../uka/ilkd/key/rule/AbstractBuiltInRuleApp.java | 3 ++- .../ilkd/key/rule/AuxiliaryContractBuilders.java | 4 ++-- .../uka/ilkd/key/rule/IfFormulaInstantiation.java | 7 ++++--- .../de/uka/ilkd/key/rule/LoopApplyHeadRule.java | 2 +- .../uka/ilkd/key/rule/LoopScopeInvariantRule.java | 1 - .../uka/ilkd/key/rule/ObserverToUpdateRule.java | 2 +- .../de/uka/ilkd/key/rule/OneStepSimplifier.java | 13 +++++++------ .../java/de/uka/ilkd/key/rule/PosTacletApp.java | 3 ++- .../main/java/de/uka/ilkd/key/rule/Taclet.java | 10 ++++++---- .../de/uka/ilkd/key/rule/WhileInvariantRule.java | 3 +-- .../uka/ilkd/key/rule/label/TermLabelMerger.java | 1 - .../ilkd/key/rule/label/TermLabelRefactoring.java | 1 - .../ilkd/key/rule/match/vm/VMTacletMatcher.java | 2 +- .../de/uka/ilkd/key/rule/merge/MergeRule.java | 1 - .../ilkd/key/speclang/BlockWellDefinedness.java | 1 - .../ilkd/key/speclang/LoopWellDefinedness.java | 1 - .../java/de/uka/ilkd/key/speclang/QueryAxiom.java | 1 - .../key/speclang/StatementWellDefinedness.java | 1 - .../key/strategy/BuiltInRuleAppContainer.java | 3 ++- .../de/uka/ilkd/key/strategy/IfInstantiator.java | 2 +- .../termProjection/AssumptionProjection.java | 1 - .../de/uka/ilkd/key/util/HelperClassForTests.java | 1 - .../ilkd/key/proof/TestTermTacletAppIndex.java | 1 - .../de/uka/ilkd/key/rule/TestApplyTaclet.java | 9 ++++----- .../ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java | 1 - .../key/util/TestEqualsModProofIrrelevancy.java | 4 ++-- .../java/org/key_project/ncore/rules/RuleApp.java | 7 ++----- .../originlabels/OriginTermLabelVisualizer.java | 3 ++- .../ilkd/key/gui/proofdiff/ProofDifference.java | 4 ++-- .../uka/ilkd/key/gui/prooftree/ProofTreeView.java | 3 ++- .../uka/ilkd/key/gui/sourceview/SourceView.java | 15 ++++++++++----- .../key/proof/reference/ReferenceSearcher.java | 4 ++-- .../key_project/slicing/DependencyTracker.java | 3 ++- .../key_project/slicing/graph/TrackedFormula.java | 11 +++++++---- 53 files changed, 82 insertions(+), 86 deletions(-) diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java index d2fba63713a..313b188cb4f 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java @@ -7,7 +7,6 @@ import java.util.Arrays; import java.util.List; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.label.FormulaTermLabel; import de.uka.ilkd.key.logic.label.TermLabel; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java index b100ac52db0..ac55939d736 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java @@ -77,7 +77,7 @@ public void updateLabels(TermLabelState state, Services services, for (IfFormulaInstantiation ifInst : ta.ifFormulaInstantiations()) { final Term assumesFml = ifInst.getConstrainedFormula(); FormulaTermLabel ifLabel = StayOnFormulaTermLabelPolicy.searchFormulaTermLabel( - assumesFml.getLabels()); + assumesFml.getLabels()); if (ifLabel != null) { ifLabels.put(ifInst.getConstrainedFormula(), ifLabel); } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java index 2ff716be73c..98360e9fe59 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java @@ -10,7 +10,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.label.FormulaTermLabel; import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.label.TermLabelState; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java index 0cd1294c599..2e06327f513 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java @@ -15,7 +15,6 @@ import de.uka.ilkd.key.java.reference.ReferencePrefix; import de.uka.ilkd.key.java.statement.MethodFrame; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.ElementaryUpdate; import de.uka.ilkd.key.logic.op.LocationVariable; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/CutHeapObjectsFeature.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/CutHeapObjectsFeature.java index 5412bdcf939..20904e34173 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/CutHeapObjectsFeature.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/CutHeapObjectsFeature.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.Equality; import de.uka.ilkd.key.logic.op.Junctor; import de.uka.ilkd.key.proof.Goal; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java index bf7847d0d35..ceeb80aa40f 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.symbolic_execution.strategy; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.JavaProfile; @@ -61,7 +60,8 @@ protected Feature setupApprovalF() { TacletApp ta = (TacletApp) app; if (ta.ifFormulaInstantiations() != null) { for (IfFormulaInstantiation ifi : ta.ifFormulaInstantiations()) { - if (ifi.getConstrainedFormula().containsLabel(SymbolicExecutionUtil.RESULT_LABEL)) { + if (ifi.getConstrainedFormula() + .containsLabel(SymbolicExecutionUtil.RESULT_LABEL)) { hasLabel = true; } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java index db636725203..55e8831a48c 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java @@ -487,7 +487,7 @@ public static SiteProofVariableValueInput createExtractReturnVariableValueSequen Term modalityTerm = services.getTermBuilder().dia(newJavaBlock, newTerm); // Get the updates from the return node which includes the value interested in. Term originalModifiedFormula = - methodReturnNode.getAppliedRuleApp().posInOccurrence().sequentLevelFormula(); + methodReturnNode.getAppliedRuleApp().posInOccurrence().sequentLevelFormula(); ImmutableList originalUpdates = TermBuilder.goBelowUpdates2(originalModifiedFormula).first; // Create Sequent to prove with new succedent. @@ -3053,7 +3053,8 @@ public static Sequent createSequentToProveWithNewSuccedent(Node node, PosInOccur } Sequent sequentToProve; sequentToProve = newSuccedentToProve != null ? originalSequentWithoutMethodFrame - .addFormula(newSuccedentToProve, false, true).sequent() : originalSequentWithoutMethodFrame; + .addFormula(newSuccedentToProve, false, true).sequent() + : originalSequentWithoutMethodFrame; if (additionalAntecedent != null) { sequentToProve = sequentToProve .addFormula(additionalAntecedent, true, false).sequent(); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java index 87719c936dc..7abfd7b8a68 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java @@ -9,7 +9,6 @@ import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.JavaBlock; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.label.TermLabelManager; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.pp.PosTableLayouter; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java index a4c7a2000ee..6cfc7b14f21 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java @@ -15,7 +15,6 @@ import de.uka.ilkd.key.java.declaration.VariableSpecification; import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java index a606ba30a28..c514cba0579 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java @@ -70,7 +70,8 @@ protected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc) { protected boolean ruleApplicationInContextAllowed(RuleApp ruleApp, PosInOccurrence pio, Goal goal) { String ruleName = ruleApp.rule().name().toString(); - if (!"andLeft".equals(ruleName)) return true; + if (!"andLeft".equals(ruleName)) + return true; return !(pio.sequentLevelFormula().op() instanceof UpdateApplication); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java index c08b8669793..a32bab1b947 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java @@ -49,7 +49,7 @@ protected void addToAntec(Semisequent semi, TermLabelState termLabelState, : "information flow taclets must have " + "exactly one add!"; final Term replacement = replacements.iterator().next(); updateStrategyInfo(services.getProof().openEnabledGoals().head(), - replacement); + replacement); super.addToAntec(semi, termLabelState, labelHint, currentSequent, pos, applicationPosInOccurrence, matchCond, goal, tacletApp, services); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java b/key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java index 3a4315f361c..a931457f419 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java @@ -8,7 +8,6 @@ import java.util.Set; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.op.QuantifiableVariable; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; 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 eec0eeb6b82..160615c9f3c 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 @@ -6,7 +6,6 @@ import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.label.TermLabelManager.TermLabelConfiguration; import de.uka.ilkd.key.logic.op.Modality; import de.uka.ilkd.key.proof.init.Profile; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java index 641dbe5d3ad..18c841493e0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java @@ -17,8 +17,8 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.Semisequent; import de.uka.ilkd.key.logic.Sequent; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.SortCollector; +import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.Equality; import de.uka.ilkd.key.logic.op.JFunction; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 786b1d1cee4..cf4e70129e7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -694,7 +694,8 @@ public static String posInOccurrence2Proof(Sequent seq, PosInOccurrence pos) { if (pos == null) { return ""; } - return " (formula \"" + seq.formulaNumberInSequent(pos.isInAntec(), pos.sequentLevelFormula()) + return " (formula \"" + + seq.formulaNumberInSequent(pos.isInAntec(), pos.sequentLevelFormula()) + "\")" + posInTerm2Proof(pos.posInTerm()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java b/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java index bd8aef204af..072a2aa0474 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java @@ -97,7 +97,8 @@ private ProspectivePartner areProspectivePartners(Goal g1, PosInOccurrence pio, } if (formula.equalsModProperty(referenceFormula, RENAMING_PROPERTY)) { - return new ProspectivePartner(referenceFormula, g1.node(), pio.sequentLevelFormula(), + return new ProspectivePartner(referenceFormula, g1.node(), + pio.sequentLevelFormula(), update1, g2.node(), sf, update2); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java b/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java index 2d137e81940..8f8429f1d06 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java @@ -205,10 +205,10 @@ private Term createPhi() { partner.getSequent(1).antecedent(), partner.getCommonFormula()); Term partnerFormula = partner.getFormula(0); Collection delta1 = computeDifference(partner.getSequent(0).succedent(), commonDelta, - partnerFormula); + partnerFormula); Term formula = partner.getFormula(1); Collection delta2 = computeDifference(partner.getSequent(1).succedent(), commonDelta, - formula); + formula); Collection gamma1 = computeDifference(partner.getSequent(0).antecedent(), commonGamma, null); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java index ad40ac5b186..278b897a38b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java @@ -338,7 +338,7 @@ private PosInOccurrence findInNewSequent(PosInOccurrence oldPos, Sequent newSequ : newSequent.succedent(); for (Term newFormula : semiSeq.asList()) { if (newFormula.equalsModProperty(oldFormula, - ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY)) { + ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY)) { return oldPos.replaceConstrainedFormula(newFormula); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java index 45cb9a98f86..e0d749cd175 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java @@ -25,7 +25,6 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.label.ParameterlessTermLabel; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java index d9745f14eb4..a0f40291d13 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java @@ -173,7 +173,8 @@ public boolean equalsModProofIrrelevancy(Object obj) { @Override public int hashCodeModProofIrrelevancy() { return Objects.hash(rule(), getHeapContext(), - ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(posInOccurrence().sequentLevelFormula()), + ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY + .hashCodeModThisProperty(posInOccurrence().sequentLevelFormula()), posInOccurrence().posInTerm()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java index 4d6addb88c5..794b40aff16 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java @@ -1395,7 +1395,7 @@ public Term setUpValidityGoal(final Goal goal, final Term[] updates, if (goal != null) { Term uAssumptions = tb.applySequential(updates, tb.and(assumptions)); goal.addFormula( - uAssumptions, true, + uAssumptions, true, false); ImmutableArray labels = TermLabelManager.instantiateLabels( @@ -1552,7 +1552,7 @@ public void setUpUsageGoal(final Goal goal, final Term[] updates, goal.addFormula(uAssumptions, true, false); Term uAssumptions1 = tb.applySequential(updates, buildUsageFormula(goal)); goal.changeFormula( - uAssumptions1, + uAssumptions1, occurrence); TermLabelManager.refactorGoal(termLabelState, services, occurrence, application.rule(), goal, null, null); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiation.java index 4dadaeb36a4..a7ab7433c88 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiation.java @@ -5,8 +5,8 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; - import de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty; + import org.key_project.util.EqualsModProofIrrelevancy; @@ -29,11 +29,12 @@ default boolean equalsModProofIrrelevancy(Object obj) { return false; } return getConstrainedFormula().equalsModProperty(that.getConstrainedFormula(), - ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY); + ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY); } @Override default int hashCodeModProofIrrelevancy() { - return getConstrainedFormula().hashCodeModProperty(ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY); + return getConstrainedFormula() + .hashCodeModProperty(ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java index acaf86c361a..43e89de8685 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java @@ -98,7 +98,7 @@ public class LoopApplyHeadRule implements BuiltInRule { Goal result = goal.split(1).head(); Term uAssumptions = tb.apply(update, tb.prog(modality.kind(), newJavaBlock, target.sub(0))); result.changeFormula( - uAssumptions, + uAssumptions, ruleApp.pio); return ImmutableSLList.nil().append(goal); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java index ed24c18b94c..85c5485e986 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java @@ -22,7 +22,6 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.ProgramPrefix; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.label.ParameterlessTermLabel; import de.uka.ilkd.key.logic.label.TermLabelManager; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java index f7b591b80ca..420e20450d0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java @@ -195,7 +195,7 @@ private ImmutableList applyForModelFields(Goal goal, ModelFieldInstantiati final Term actualSelfNotNull = tb.not(tb.equals(inst.receiver, tb.NULL())); Term uAssumptions = tb.apply(inst.update, actualSelfNotNull, null); nullGoal.changeFormula( - uAssumptions, + uAssumptions, ruleApp.posInOccurrence()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java index 1f06d29320f..19d726d810b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java @@ -409,9 +409,9 @@ private RuleApp makeReplaceKnownTacletApp(Term formula, boolean inAntecedent, PosInOccurrence applicatinPIO = new PosInOccurrence(formula, PosInTerm.getTopLevel(), // TODO: This - // should be - // the precise - // sub term + // should be + // the precise + // sub term inAntecedent); // It is required to create a new PosInOccurrence because formula and // pio.constrainedFormula().formula() are only equals module // renamings and term labels @@ -465,7 +465,7 @@ private Instantiation computeInstantiation(Services services, PosInOccurrence os if (!ante.equals(cf)) { if (ante.op() != Junctor.TRUE) { context.put(new TermReplacementKey(ante), - new PosInOccurrence(ante, PosInTerm.getTopLevel(), true)); + new PosInOccurrence(ante, PosInTerm.getTopLevel(), true)); } } } @@ -473,7 +473,7 @@ private Instantiation computeInstantiation(Services services, PosInOccurrence os if (!succ.equals(cf)) { if (succ.op() != Junctor.FALSE) { context.put(new TermReplacementKey(succ), - new PosInOccurrence(succ, PosInTerm.getTopLevel(), false)); + new PosInOccurrence(succ, PosInTerm.getTopLevel(), false)); } } } @@ -575,7 +575,8 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) { } // applicable to the formula? - return applicableTo(goal.proof().getServices(), pio.sequentLevelFormula(), pio.isInAntec(), goal, + return applicableTo(goal.proof().getServices(), pio.sequentLevelFormula(), pio.isInAntec(), + goal, null); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java index 624ec722ac1..0baf6550866 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java @@ -320,7 +320,8 @@ public boolean equalsModProofIrrelevancy(Object o) { @Override public int hashCodeModProofIrrelevancy() { return Objects.hash(super.hashCodeModProofIrrelevancy(), - ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(pos.sequentLevelFormula()), + ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY + .hashCodeModThisProperty(pos.sequentLevelFormula()), pos.posInTerm()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java index 0d1fad9dac8..f110d474dd5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java @@ -498,8 +498,9 @@ public boolean equalsModProofIrrelevancy(Object o) { while (!if1.isEmpty() && !if2.isEmpty()) { Term term = if1.head(); Term head = if2.head(); - if (!(boolean) ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY. - equalsModThisProperty(term, head)) break; + if (!(boolean) ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY + .equalsModThisProperty(term, head)) + break; if1 = if1.tail(); if2 = if2.tail(); } @@ -534,7 +535,8 @@ public int hashCode() { public int hashCodeModProofIrrelevancy() { if (hashcode2 == 0) { Term term = ifSequent.getFormulabyNr(1); - hashcode2 = ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(term); + hashcode2 = + ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(term); if (hashcode2 == 0) { hashcode2 = -1; } @@ -960,7 +962,7 @@ public enum TacletOperation { */ @Override public @NonNull ImmutableList apply(Goal goal, Services services, RuleApp tacletApp) { - return getExecutor().apply((Goal)goal, services, tacletApp); + return getExecutor().apply((Goal) goal, services, tacletApp); } public TacletExecutor getExecutor() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java index a9a4777a389..08a5af12b99 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java @@ -35,7 +35,6 @@ import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.label.ParameterlessTermLabel; @@ -624,7 +623,7 @@ private void prepareBodyPreservesBranch(TermLabelState termLabelState, Services Term uAssumptions = tb.applySequential(uBeforeLoopDefAnonVariant, guardTrueBody); bodyGoal.changeFormula( - uAssumptions, + uAssumptions, ruleApp.posInOccurrence()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelMerger.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelMerger.java index 4f79dfac9ed..a1e0d567191 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelMerger.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelMerger.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.label.TermLabelManager; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java index e974f5759d4..606cc7262a0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java @@ -7,7 +7,6 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.label.LabelCollection; import de.uka.ilkd.key.logic.label.TermLabel; 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 56ffd4da8d9..409bb2008e9 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 @@ -209,7 +209,7 @@ public final MatchConditions matchIf(Iterable p_toMatch, assert itIfSequent.hasNext() : "p_toMatch and assumes sequent must have same number of elements"; newMC = matchIf(ImmutableSLList.nil().prepend(candidateInst), - itIfSequent.next(), p_matchCond, p_services).getMatchConditions(); + itIfSequent.next(), p_matchCond, p_services).getMatchConditions(); if (newMC.isEmpty()) { return null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java index 5b3e3f278f5..81a338bfeb5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java @@ -15,7 +15,6 @@ import de.uka.ilkd.key.logic.PosInTerm; import de.uka.ilkd.key.logic.Semisequent; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.*; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java index 91baa0bf44c..bc74bf244c8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java @@ -9,7 +9,6 @@ import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.java.declaration.modifier.VisibilityModifier; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.IObserverFunction; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java index 9ab8f8ba09f..b9fb0c6ffe6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java @@ -9,7 +9,6 @@ import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.java.declaration.modifier.VisibilityModifier; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.IObserverFunction; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java index c4613779a6c..8e5aaccc030 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java @@ -19,7 +19,6 @@ import de.uka.ilkd.key.logic.Semisequent; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.ProgramSVSort; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java index 41cd5cf0936..0e9df5a1589 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java @@ -9,7 +9,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.*; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/BuiltInRuleAppContainer.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/BuiltInRuleAppContainer.java index c6215eb40df..a853dea7996 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/BuiltInRuleAppContainer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/BuiltInRuleAppContainer.java @@ -64,7 +64,8 @@ private boolean isStillApplicable(Goal goal) { // the formula does not exist anymore, bail out return false; } else { - return topPos.sequentLevelFormula().equals(applicationPosition.sequentLevelFormula()); + return topPos.sequentLevelFormula() + .equals(applicationPosition.sequentLevelFormula()); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiator.java index e1df64a2f4e..c64397f7005 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiator.java @@ -218,7 +218,7 @@ private void findIfFormulaInstantiationsHelp(ImmutableList p_ifSeqTail, final ImmutableArray formulas = getTerms(antec, !lastIfFormula || p_alreadyMatchedNewFor); final IfMatchResult mr = getTaclet().getMatcher().matchIf(formulas, - p_ifSeqTail.head(), p_matchCond, getServices()); + p_ifSeqTail.head(), p_matchCond, getServices()); // For each matching formula call the method again to match // the remaining terms diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/AssumptionProjection.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/AssumptionProjection.java index dfe2bd6d0ac..29f2bb0ccf7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/AssumptionProjection.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/AssumptionProjection.java @@ -5,7 +5,6 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.RuleApp; import de.uka.ilkd.key.rule.TacletApp; diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/HelperClassForTests.java b/key.core/src/main/java/de/uka/ilkd/key/util/HelperClassForTests.java index 276bc899629..e6ad15022b4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/HelperClassForTests.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/HelperClassForTests.java @@ -14,7 +14,6 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.IObserverFunction; import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.proof.Proof; diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/TestTermTacletAppIndex.java b/key.core/src/test/java/de/uka/ilkd/key/proof/TestTermTacletAppIndex.java index e68ed574c61..1fd6e267c92 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/TestTermTacletAppIndex.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/TestTermTacletAppIndex.java @@ -11,7 +11,6 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.logic.PosInTerm; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.proof.PrefixTermTacletAppIndexCacheImpl.CacheKey; import de.uka.ilkd.key.proof.rulefilter.SetRuleFilter; import de.uka.ilkd.key.proof.rulefilter.TacletFilter; diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java b/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java index 0d6750829f0..30a30c21435 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java @@ -69,7 +69,7 @@ private static Semisequent parseTermForSemisequent(String t) { return Semisequent.EMPTY_SEMISEQUENT; } return Semisequent.EMPTY_SEMISEQUENT.insert(0, - TacletForTests.parseTerm(t)).semisequent(); + TacletForTests.parseTerm(t)).semisequent(); } @BeforeEach @@ -314,12 +314,12 @@ public void testNoFindTacletWithoutIf() { Sequent seq2 = goals.head().sequent(); if (!seq1.antecedent().isEmpty() && seq1.antecedent().getFirst().equals(t_c)) { assertTrue( - seq2.succedent().getFirst().equals(t_c) + seq2.succedent().getFirst().equals(t_c) || seq2.succedent().get(1).equals(t_c), "D is in antecedent of 1st goal but not in succedent of 2nd"); } else { assertTrue( - seq1.succedent().getFirst().equals(t_c) + seq1.succedent().getFirst().equals(t_c) || seq1.succedent().get(1).equals(t_c), "D is not in antecedent and not in succedent " + "of first new goal"); assertEquals(seq2.antecedent().getFirst(), t_c, @@ -893,8 +893,7 @@ public void testRemoveEmptyBlock() { TacletForTests.parsePrg("{try{while (1==1) {if (1==2) {break;}} return 1==3; " + "int i=17; } catch (Exception e) { return null;}}"); - ProgramElement is = goals.head().sequent(). - getFormulabyNr(1).javaBlock().program(); + ProgramElement is = goals.head().sequent().getFormulabyNr(1).javaBlock().program(); assertTrue(expected.equalsModRenaming(is, new NameAbstractionTable()), "Expected:" + expected + "\n but was:" + is); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java index a94b16e5ba6..1c4b18b9fcc 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java @@ -18,7 +18,6 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.nparser.KeyIO; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.ProofSaver; diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestEqualsModProofIrrelevancy.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestEqualsModProofIrrelevancy.java index 5b8fea09959..5927c33693d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestEqualsModProofIrrelevancy.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestEqualsModProofIrrelevancy.java @@ -51,8 +51,8 @@ void testJavaProof() throws Exception { for (int j = 1; j <= node1.sequent().size(); j++) { Term sf1 = node1.sequent().getFormulabyNr(j); Term sf2 = node2.sequent().getFormulabyNr(j); - Assertions.assertTrue(ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY. - equalsModThisProperty(sf1, sf2)); + Assertions.assertTrue(ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY + .equalsModThisProperty(sf1, sf2)); } if (node1.getAppliedRuleApp() != null) { Assertions.assertTrue( diff --git a/key.ncore.calculus/src/main/java/org/key_project/ncore/rules/RuleApp.java b/key.ncore.calculus/src/main/java/org/key_project/ncore/rules/RuleApp.java index a13217ee91d..f60e443475b 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/ncore/rules/RuleApp.java +++ b/key.ncore.calculus/src/main/java/org/key_project/ncore/rules/RuleApp.java @@ -3,10 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.ncore.rules; -import org.key_project.ncore.proof.ProofGoal; -import org.key_project.util.collection.ImmutableList; -import org.jspecify.annotations.Nullable; public interface RuleApp { /** @@ -21,8 +18,8 @@ public interface RuleApp { * @param goal the Goal where to apply the rule * @return list of new created goals */ -// @Nullable -// ImmutableList execute(G goal); + // @Nullable + // ImmutableList execute(G goal); /** * returns true if all variables are instantiated diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java index da350938e05..0be5786e726 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java @@ -419,7 +419,8 @@ private PosInOccurrence convertPio(PosInOccurrence pio) { completePos = completePos.down(it.next()); } - return new PosInOccurrence(termPio.sequentLevelFormula(), completePos, termPio.isInAntec()); + return new PosInOccurrence(termPio.sequentLevelFormula(), completePos, + termPio.isInAntec()); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java index df10272ae35..b10161c32e9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java @@ -46,8 +46,8 @@ public static ProofDifference create(Node left, Node right, Function initialise(Function printer, Semisequent semisequent) { return semisequent.asList().stream().map(it -> { - return printer.apply(it); - }) + return printer.apply(it); + }) .collect(Collectors.toList()); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index 01a4f234c73..329ac53aae7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -959,7 +959,8 @@ public void valueChanged(TreeSelectionEvent e) { var ossParentNode = ((GUIProofTreeNode) ossNode.getParent()); var newSequent = ossParentNode.getNode().sequent(); var modifiedSequent = newSequent - .replaceFormula(ossNode.getFormulaNr(), pio.sequentLevelFormula()).sequent(); + .replaceFormula(ossNode.getFormulaNr(), pio.sequentLevelFormula()) + .sequent(); mediator.getSelectionModel().setSelectedSequentAndRuleApp( ossParentNode.getNode(), modifiedSequent, ossNode.getRuleApp()); } else { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java index c194b08df31..6e8fea862a1 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java @@ -769,21 +769,26 @@ protected void doDefaultAction(SourceElement el) { } else { // the method is declared without a body // -> we try to show the file either way - IProgramMethod pm = mb.getProgramMethod(services); + IProgramMethod pm = + mb.getProgramMethod(services); if (pm != null) { posInf = pm.getPositionInfo(); } } if (posInf != null && posInf.getURI().isPresent()) { - // sometimes the useful file info is only stored in + // sometimes the useful file info is only stored + // in // parentClassURI for some reason ... if (posInf.getURI().isPresent()) { node.proof() - .lookup(ProofJavaSourceCollection.class) - .addRelevantFile(posInf.getURI().get()); + .lookup( + ProofJavaSourceCollection.class) + .addRelevantFile( + posInf.getURI().get()); } else if (posInf.getParentClassURI() != null) { node.proof() - .lookup(ProofJavaSourceCollection.class) + .lookup( + ProofJavaSourceCollection.class) .addRelevantFile( posInf.getParentClassURI()); } diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java index fe7de1ae300..387f6eb45c2 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java @@ -148,8 +148,8 @@ private static boolean containedIn(Semisequent superset, Semisequent subset) { for (Term sf : subset) { boolean found = false; for (Term sf2 : superset) { - if (ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY. - equalsModThisProperty(sf2, sf)) { + if (ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.equalsModThisProperty(sf2, + sf)) { found = true; break; } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index 4bf1ab4e822..6ed6b7cc945 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -161,7 +161,8 @@ private List> inputsOfNode(Node n, Set // should only happen if the formula is the initial proof obligation if (!proof.root().sequent().contains(in.sequentLevelFormula())) { throw new IllegalStateException( - "found formula that was not produced by any rule! " + in.sequentLevelFormula()); + "found formula that was not produced by any rule! " + + in.sequentLevelFormula()); } TrackedFormula formula = new TrackedFormula(in.sequentLevelFormula(), loc, in.isInAntec(), diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFormula.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFormula.java index dbf6ac4b341..4d118f5b973 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFormula.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/TrackedFormula.java @@ -71,7 +71,7 @@ public String toString(boolean abbreviated, boolean omitBranch) { return Integer.toHexString(hashCode()); } String term = LogicPrinter.quickPrintTerm( - formula, + formula, services, true, // pretty print true // using unicode symbols @@ -110,13 +110,16 @@ public boolean equalsModProofIrrelevancy(Object o) { return false; } TrackedFormula that = (TrackedFormula) o; - return inAntec == that.inAntec && ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY. - equalsModThisProperty(formula, that.formula) + return inAntec == that.inAntec + && ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY + .equalsModThisProperty(formula, that.formula) && Objects.equals(branchLocation, that.branchLocation); } @Override public int hashCodeModProofIrrelevancy() { - return Objects.hash(inAntec, ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(formula), branchLocation); + return Objects.hash(inAntec, + ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(formula), + branchLocation); } }