From 34ee37a18c69c3b42cdb5e1fe07b4c6a66d21b2c Mon Sep 17 00:00:00 2001
From: Richard Bubel
Date: Wed, 4 Oct 2023 21:49:03 +0200
Subject: [PATCH 1/5] Some general minor code quality improvements
---
.../proof/InstantiationProposerCollection.java | 3 +--
.../de/uka/ilkd/key/proof/ProgVarReplacer.java | 1 -
.../SVInstantiationExceptionWithPosition.java | 2 +-
.../de/uka/ilkd/key/proof/TacletAppIndex.java | 2 +-
.../de/uka/ilkd/key/proof/TacletIndex.java | 6 ++----
.../key/proof/init/DependencyContractPO.java | 3 +--
.../proof/init/FunctionalBlockContractPO.java | 5 ++---
.../proof/init/FunctionalLoopContractPO.java | 5 ++---
.../init/FunctionalOperationContractPO.java | 4 ++--
.../key/proof/init/KeYUserProblemFile.java | 6 +++---
.../key/proof/init/ProblemInitializer.java | 9 ++-------
.../ilkd/key/proof/init/WellDefinednessPO.java | 14 ++++++--------
.../de/uka/ilkd/key/proof/io/EnvInput.java | 3 +--
.../proof/io/IntermediateProofReplayer.java | 1 -
.../de/uka/ilkd/key/proof/io/LDTInput.java | 6 +++---
.../de/uka/ilkd/key/proof/io/ProofSaver.java | 2 +-
.../proof/io/consistency/MemoryFileRepo.java | 6 +++---
.../de/uka/ilkd/key/prover/StopCondition.java | 18 +++++++++---------
.../ilkd/key/prover/impl/ApplyStrategy.java | 9 ++++-----
.../key/prover/impl/ApplyStrategyInfo.java | 2 +-
.../key/prover/impl/DefaultGoalChooser.java | 7 ++-----
.../key/prover/impl/DepthFirstGoalChooser.java | 4 +---
.../prover/impl/SingleRuleApplicationInfo.java | 3 +--
.../key/strategy/IfInstantiationCachePool.java | 6 +++---
.../ilkd/key/strategy/TacletAppContainer.java | 13 +++++--------
.../uka/ilkd/key/strategy/TopRuleAppCost.java | 2 +-
.../strategy/feature/AbstractBetaFeature.java | 2 +-
.../feature/AppliedRuleAppsNameCache.java | 2 +-
.../feature/ContainsQuantifierFeature.java | 2 +-
.../strategy/feature/ContainsTermFeature.java | 8 +++-----
.../strategy/feature/DirectlyBelowFeature.java | 2 +-
.../feature/DirectlyBelowSymbolFeature.java | 2 +-
.../key/strategy/feature/FindDepthFeature.java | 2 +-
.../feature/MonomialsSmallerThanFeature.java | 4 +---
.../key/strategy/feature/ScaleFeature.java | 7 +++++--
.../feature/TrivialMonomialLCRFeature.java | 2 +-
.../findprefix/AntecSuccPrefixChecker.java | 13 ++++---------
.../instantiator/SVInstantiationCP.java | 7 +++----
.../EqualityConstraint.java | 2 +-
.../quantifierHeuristics/Metavariable.java | 2 ++
.../PredictCostProver.java | 2 +-
.../quantifierHeuristics/TriggersSet.java | 2 +-
.../quantifierHeuristics/TwoSidedMatching.java | 4 ++--
.../SVInstantiationProjection.java | 9 ++++-----
.../TermConstructionProjection.java | 2 +-
.../strategy/termfeature/EqTermFeature.java | 2 +-
.../termfeature/IsInductionVariable.java | 2 +-
.../MultiplesModEquationsGenerator.java | 4 ++--
.../key/gui/WindowUserInterfaceControl.java | 13 +++----------
.../ilkd/key/gui/actions/QuickSaveAction.java | 17 ++++++++---------
.../AbstractMediatorUserInterfaceControl.java | 6 +-----
51 files changed, 109 insertions(+), 153 deletions(-)
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/InstantiationProposerCollection.java b/key.core/src/main/java/de/uka/ilkd/key/proof/InstantiationProposerCollection.java
index 4b580513eab..1e19ff05171 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/InstantiationProposerCollection.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/InstantiationProposerCollection.java
@@ -29,8 +29,7 @@ public void add(InstantiationProposer proposer) {
public String getProposal(TacletApp app, SchemaVariable var, Services services, Node undoAnchor,
ImmutableList previousProposals) {
- for (InstantiationProposer proposer1 : proposers) {
- InstantiationProposer proposer = proposer1;
+ for (InstantiationProposer proposer : proposers) {
String proposal =
proposer.getProposal(app, var, services, undoAnchor, previousProposals);
if (proposal != null) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java
index 7c7d914118f..5db7a4503b1 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java
@@ -19,7 +19,6 @@
import de.uka.ilkd.key.rule.NoPosTacletApp;
import de.uka.ilkd.key.rule.inst.*;
-import org.key_project.util.collection.*;
import org.key_project.util.collection.DefaultImmutableSet;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java b/key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java
index 87726d6736a..023713557bd 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java
@@ -61,7 +61,7 @@ public String toString() {
@Nullable
@Override
- public Location getLocation() throws MalformedURLException {
+ public Location getLocation() {
return new Location(null, position);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java
index 9f4cce98b73..aae1773faca 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletAppIndex.java
@@ -58,7 +58,7 @@ public class TacletAppIndex {
*/
private RuleFilter ruleFilter;
- private State state;
+ private final State state;
private final Map cache;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java
index eacc5b9fba8..ae6dc4e8358 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java
@@ -379,7 +379,7 @@ private ImmutableList getListHelp(
* @param second the second list
* @return the merged list
*/
- private final ImmutableList merge(ImmutableList first,
+ private ImmutableList merge(ImmutableList first,
final ImmutableList second) {
if (second == null) {
return first;
@@ -579,9 +579,7 @@ private static class PrefixOccurrences {
* resets the occurred field to 'nothing has occurred'
*/
public void reset() {
- for (int i = 0; i < PREFIXTYPES; i++) {
- occurred[i] = false;
- }
+ Arrays.fill(occurred, 0, PREFIXTYPES, false);
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
index dc3b8f1fcae..616c51e7d7e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
@@ -304,8 +304,7 @@ public void fillSaveProperties(Properties properties) {
* @return The instantiated proof obligation.
* @throws IOException Occurred Exception.
*/
- public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties)
- throws IOException {
+ public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
String contractName = properties.getProperty("contract");
int proofNum = 0;
String baseContractName = null;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
index e2f4fef4fb6..5e3fe8fba23 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
@@ -82,8 +82,7 @@ public FunctionalBlockContractPO(InitConfig initConfig, FunctionalBlockContract
* @return The instantiated proof obligation.
* @throws IOException Occurred Exception.
*/
- public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties)
- throws IOException {
+ public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
String contractName = properties.getProperty("contract");
int proofNum = 0;
String baseContractName = null;
@@ -339,7 +338,7 @@ public boolean equals(Object obj) {
}
@Override
- public void readProblem() throws ProofInputException {
+ public void readProblem() {
assert proofConfig == null;
final boolean makeNamesUnique = true;
final Services services = postInit();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
index 5d7cde7ce8b..9d47742b614 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
@@ -82,8 +82,7 @@ public FunctionalLoopContractPO(InitConfig initConfig, FunctionalLoopContract co
* @return The instantiated proof obligation.
* @throws IOException Occurred Exception.
*/
- public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties)
- throws IOException {
+ public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
String contractName = properties.getProperty("contract");
int proofNum = 0;
String baseContractName = null;
@@ -161,7 +160,7 @@ public boolean equals(Object obj) {
}
@Override
- public void readProblem() throws ProofInputException {
+ public void readProblem() {
assert proofConfig == null;
final boolean makeNamesUnique = true;
final Services services = postInit();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java
index a8616adcf5a..ca350db84b5 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java
@@ -62,7 +62,7 @@
*/
public class FunctionalOperationContractPO extends AbstractOperationPO implements ContractPO {
public static final Map TRANSACTION_TAGS =
- new LinkedHashMap();
+ new LinkedHashMap<>();
private final FunctionalOperationContract contract;
@@ -134,7 +134,7 @@ protected ImmutableList buildOperationBlocks(
ImmutableList formalParVars, ProgramVariable selfVar,
ProgramVariable resultVar, Services services) {
final StatementBlock[] result = new StatementBlock[4];
- final ImmutableArray formalArray = new ImmutableArray(
+ final ImmutableArray formalArray = new ImmutableArray<>(
formalParVars.toArray(new ProgramVariable[formalParVars.size()]));
if (getContract().getTarget().isConstructor()) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
index b561e08094e..6e9072ec1ff 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
@@ -159,7 +159,7 @@ public String getProofObligation() {
}
@Override
- public ProofAggregate getPO() throws ProofInputException {
+ public ProofAggregate getPO() {
assert problem != null;
String name = name();
ProofSettings settings = getPreferences();
@@ -181,7 +181,7 @@ public boolean hasProofScript() {
return getParseContext().findProofScript() != null;
}
- public Triple readProofScript() throws ProofInputException {
+ public Triple readProofScript() {
return getParseContext().findProofScript();
}
@@ -242,7 +242,7 @@ public Profile getProfile() {
* is defined by the file.
* @throws Exception Occurred Exception.
*/
- private Profile readProfileFromFile() throws Exception {
+ private Profile readProfileFromFile() {
@Nonnull
ProblemInformation pi = getProblemInformation();
String profileName = pi.getProfile();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
index c94b1c72336..ec0cd354c57 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
@@ -239,11 +239,7 @@ private void readJava(EnvInput envInput, InitConfig initConfig) throws ProofInpu
final String javaPath = envInput.readJavaPath();
final List classPath = envInput.readClassPath();
final File bootClassPath;
- try {
- bootClassPath = envInput.readBootClassPath();
- } catch (IOException ioe) {
- throw new ProofInputException(ioe);
- }
+ bootClassPath = envInput.readBootClassPath();
final Includes includes = envInput.readIncludes();
@@ -384,8 +380,7 @@ private void populateNamespaces(Proof proof) {
}
// what is the purpose of this method?
- private InitConfig determineEnvironment(ProofOblInput po, InitConfig initConfig)
- throws ProofInputException {
+ private InitConfig determineEnvironment(ProofOblInput po, InitConfig initConfig) {
// TODO: what does this actually do?
ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().updateChoices(initConfig.choiceNS(),
false);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
index c18503bd72f..4a37555543e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
@@ -199,13 +199,12 @@ private void register(Variables vars, Services proofServices) {
protected ImmutableSet selectClassAxioms(KeYJavaType kjt) {
ImmutableSet result = DefaultImmutableSet.nil();
for (ClassAxiom axiom : specRepos.getClassAxioms(kjt)) {
- if (axiom instanceof ClassAxiom && check instanceof ClassWellDefinedness cwd) {
- final ClassAxiom classAxiom = axiom;
+ if (check instanceof ClassWellDefinedness cwd) {
final String kjtName = cwd.getKJT().getFullName();
final String invName = "in " + cwd.getKJT().getName();
- if (!classAxiom.getName().endsWith(invName)
- && !classAxiom.getName().endsWith(kjtName)) {
- result = result.add(classAxiom);
+ if (!axiom.getName().endsWith(invName)
+ && !axiom.getName().endsWith(kjtName)) {
+ result = result.add(axiom);
}
} else {
result = result.add(axiom);
@@ -227,7 +226,7 @@ public KeYJavaType getKJT() {
}
@Override
- public void readProblem() throws ProofInputException {
+ public void readProblem() {
assert proofConfig == null;
final Services proofServices = postInit();
@@ -302,8 +301,7 @@ public void fillSaveProperties(Properties properties) {
* @return The instantiated proof obligation.
* @throws IOException Occurred Exception.
*/
- public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties)
- throws IOException {
+ public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
String contractName = properties.getProperty("wd check");
final Contract contract =
initConfig.getServices().getSpecificationRepository().getContractByName(contractName);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java
index b936a0216e2..f92d19995fa 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java
@@ -4,7 +4,6 @@
package de.uka.ilkd.key.proof.io;
import java.io.File;
-import java.io.IOException;
import java.util.List;
import javax.annotation.Nonnull;
import javax.annotation.Nullable;
@@ -71,7 +70,7 @@ public interface EnvInput {
*
* @throws
*/
- File readBootClassPath() throws IOException;
+ File readBootClassPath();
/**
* Reads the input using the given modification strategy, i.e., parts of the input do not modify
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
index e0f791f1f3a..3e49bbc2bd8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
@@ -45,7 +45,6 @@
import de.uka.ilkd.key.settings.ProofIndependentSMTSettings;
import de.uka.ilkd.key.settings.ProofIndependentSettings;
import de.uka.ilkd.key.smt.*;
-import de.uka.ilkd.key.smt.SMTRuleApp;
import de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth;
import de.uka.ilkd.key.speclang.Contract;
import de.uka.ilkd.key.speclang.OperationContract;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java
index adda0b3cb57..4013351ffbf 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java
@@ -85,14 +85,14 @@ public Includes readIncludes() throws ProofInputException {
@Override
- public String readJavaPath() throws ProofInputException {
+ public String readJavaPath() {
return "";
}
// no class path elements here
@Override
- public List readClassPath() throws ProofInputException {
+ public List readClassPath() {
return null;
}
@@ -111,7 +111,7 @@ public File readBootClassPath() {
* declared sorts in all rules, e.g.
*/
@Override
- public ImmutableSet read() throws ProofInputException {
+ public ImmutableSet read() {
if (initConfig == null) {
throw new IllegalStateException("LDTInput: InitConfig not set.");
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java
index e2b95a1ca41..8cfcae13817 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java
@@ -87,7 +87,7 @@ protected void save(File file) throws IOException {
save(new FileOutputStream(file));
}
- public String save() throws IOException {
+ public String save() {
String errorMsg = null;
try {
save(file);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/MemoryFileRepo.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/MemoryFileRepo.java
index c096bacf011..f735f856497 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/MemoryFileRepo.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/MemoryFileRepo.java
@@ -19,19 +19,19 @@
public class MemoryFileRepo extends AbstractFileRepo {
@Override
- public InputStream getInputStream(Path path) throws IOException {
+ public InputStream getInputStream(Path path) {
// TODO Auto-generated method stub
return null;
}
@Override
- public InputStream getInputStream(RuleSource ruleSource) throws IOException {
+ public InputStream getInputStream(RuleSource ruleSource) {
// TODO Auto-generated method stub
return null;
}
@Override
- public InputStream getInputStream(URL url) throws IOException {
+ public InputStream getInputStream(URL url) {
// TODO Auto-generated method stub
return null;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/StopCondition.java b/key.core/src/main/java/de/uka/ilkd/key/prover/StopCondition.java
index 311ff819352..f28599cc582 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/prover/StopCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/prover/StopCondition.java
@@ -17,16 +17,16 @@
*
*
* The first check is done before a rule is applied on a {@link Goal} via
- * {@link #isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)}. If this
+ * {@link #isGoalAllowed(int, long, Proof, long, int, Goal)}. If this
* method returns {@code false} the strategy stops and the reason shown to the user is computed via
- * {@link #getGoalNotAllowedMessage(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)}.
+ * {@link #getGoalNotAllowedMessage(int, long, Proof, long, int, Goal)}.
*
*
* The second check is after a rule was applied via
- * {@link #shouldStop(ApplyStrategy, int, long, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)}.
+ * {@link #shouldStop(int, long, Proof, long, int, SingleRuleApplicationInfo)}.
* If this method returns {@code true} the strategy stops and the reason shown to the user is
* computed via
- * {@link #getStopMessage(ApplyStrategy, int, long, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)}.
+ * {@link #getStopMessage(int, long, Proof, long, int, SingleRuleApplicationInfo)}.
*
*
* Attention: It is possible that an {@link StopCondition} has to check one {@link Goal}
@@ -71,7 +71,7 @@ boolean isGoalAllowed(int maxApplications, long timeout, Proof proof, long start
/**
* Returns the reason why the previous check via
- * {@link #isGoalAllowed(ApplyStrategy, int, long, Proof, GoalChooser, long, int, Goal)} has
+ * {@link #isGoalAllowed(int, long, Proof, long, int, Goal)} has
* stopped the apply strategy.
*
* @param maxApplications The defined maximal number of rules to apply. Can be different to
@@ -83,7 +83,7 @@ boolean isGoalAllowed(int maxApplications, long timeout, Proof proof, long start
* {@link System#currentTimeMillis()}
* @param countApplied The number of already applied rules.
* @param goal The current {@link Goal} on which the next rule will be applied.
- * @return
+ * @return description of the reason why automatic proof search has stopped
*/
String getGoalNotAllowedMessage(int maxApplications, long timeout, Proof proof,
long startTime, int countApplied, Goal goal);
@@ -107,8 +107,8 @@ boolean shouldStop(int maxApplications, long timeout, Proof proof, long startTim
int countApplied, SingleRuleApplicationInfo singleRuleApplicationInfo);
/**
- * Returns a human readable message which explains why the previous
- * {@link #shouldStop(ApplyStrategy, Proof, GoalChooser, long, int, SingleRuleApplicationInfo)}
+ * Returns a human-readable message which explains why the previous
+ * {@link #shouldStop(int, long, Proof, long, int, SingleRuleApplicationInfo)}
* has stopped the strategy.
*
* @param maxApplications The defined maximal number of rules to apply. Can be different to
@@ -120,7 +120,7 @@ boolean shouldStop(int maxApplications, long timeout, Proof proof, long startTim
* {@link System#currentTimeMillis()}
* @param countApplied The number of already applied rules.
* @param singleRuleApplicationInfo An optional {@link SingleRuleApplicationInfo}.
- * @return The human readable message which explains the stop reason.
+ * @return The human-readable message which explains the stop reason.
*/
String getStopMessage(int maxApplications, long timeout, Proof proof, long startTime,
int countApplied, SingleRuleApplicationInfo singleRuleApplicationInfo);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategy.java
index c09e1868381..05b6f74d9dd 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategy.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategy.java
@@ -55,7 +55,7 @@ public class ApplyStrategy extends AbstractProverCore {
/** time in ms after which rule application shall be aborted, -1 disables timeout */
private long timeout = -1;
- /** true if the prover should stop as soon as a non closable goal is detected */
+ /** true if the prover should stop as soon as a non-closable goal is detected */
private boolean stopAtFirstNonClosableGoal;
/** the number of (so far) closed goal by the current running strategy */
private int closedGoals;
@@ -67,7 +67,7 @@ public class ApplyStrategy extends AbstractProverCore {
private GoalChooser goalChooser;
// Please create this object beforehand and re-use it.
- // Otherwise the addition/removal of the InteractiveProofListener
+ // Otherwise, the addition/removal of the InteractiveProofListener
// can cause a ConcurrentModificationException during ongoing operation
public ApplyStrategy(GoalChooser defaultGoalChooser) {
this.defaultGoalChooser = defaultGoalChooser;
@@ -76,7 +76,7 @@ public ApplyStrategy(GoalChooser defaultGoalChooser) {
/**
* applies rules that are chosen by the active strategy
*
- * @return true iff a rule has been applied, false otherwise
+ * @return information whether the rule application was successful or not
*/
private synchronized SingleRuleApplicationInfo applyAutomaticRule(final GoalChooser goalChooser,
final StopCondition stopCondition, boolean stopAtFirstNonClosableGoal) {
@@ -110,7 +110,6 @@ private synchronized SingleRuleApplicationInfo applyAutomaticRule(final GoalChoo
return new SingleRuleApplicationInfo(
"No more rules automatically applicable to any goal.", g, app);
} else {
- assert g != null;
var time = System.nanoTime();
try {
g.apply(app);
@@ -287,7 +286,7 @@ private ApplyStrategyInfo executeStrategy(ProofTreeListener treeListener) {
ProofListener pl = new ProofListener();
proof.addRuleAppListener(pl);
- ApplyStrategyInfo result = null;
+ ApplyStrategyInfo result;
try {
result = doWork(goalChooser, stopCondition);
} finally {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategyInfo.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategyInfo.java
index 91ee74b59e9..4d62b6f67cb 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategyInfo.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategyInfo.java
@@ -11,7 +11,7 @@
* instance that started the strategies.
*
* It contains statistic information about the number of applied rules, time needed or number of
- * closed goals. In case the rule application stopped at a non closeable goal, this goal is also
+ * closed goals. In case the rule application stopped at a non-closeable goal, this goal is also
* stored to allow the caller to e.g. present it to the user for interaction.
*
* In case of an unexpected, the thrown exception can be also retrieved from this container.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultGoalChooser.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultGoalChooser.java
index e6eb0ead528..b12308891d9 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultGoalChooser.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultGoalChooser.java
@@ -82,8 +82,7 @@ protected void setupGoals(ImmutableList p_goals) {
}
} else {
- for (Goal p_goal : p_goals) {
- final Goal goal = p_goal;
+ for (final Goal goal : p_goals) {
selectedList = selectedList.prepend(goal);
}
@@ -218,9 +217,7 @@ protected void updateGoalListHelp(Node node, ImmutableList newGoals) {
protected ImmutableList insertNewGoals(ImmutableList newGoals,
ImmutableList prevGoalList) {
- for (Goal newGoal : newGoals) {
- final Goal g = newGoal;
-
+ for (final Goal g : newGoals) {
if (proof.openGoals().contains(g)) {
if (!allGoalsSatisfiable) {
goalList = goalList.prepend(g);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DepthFirstGoalChooser.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DepthFirstGoalChooser.java
index f833a5ba63c..9205fa90c4a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DepthFirstGoalChooser.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/DepthFirstGoalChooser.java
@@ -54,9 +54,7 @@ public Goal getNextGoal() {
protected ImmutableList insertNewGoals(ImmutableList newGoals,
ImmutableList prevGoalList) {
- for (Goal newGoal : newGoals) {
- final Goal g = newGoal;
-
+ for (final Goal g : newGoals) {
if (proof.openGoals().contains(g)) {
// if (!allGoalsSatisfiable)
// goalList = goalList.prepend(g);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/SingleRuleApplicationInfo.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/SingleRuleApplicationInfo.java
index feb45173bb2..6f9fc4f0468 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/SingleRuleApplicationInfo.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/SingleRuleApplicationInfo.java
@@ -8,8 +8,7 @@
/**
* Instances of this class are used to store if a rule could be applied automatically and if not to
- * store the reason why no rule applications could be performed. Because of performance reason the
- * success case returns the singleton {@link SingleRuleApplicationInfo#SUCCESS}
+ * store the reason why no rule applications could be performed.
*/
public class SingleRuleApplicationInfo {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiationCachePool.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiationCachePool.java
index 43646599e00..9ef84de7eff 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiationCachePool.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiationCachePool.java
@@ -18,10 +18,10 @@
/**
* Direct-mapped cache of lists of formulas (potential instantiations of if-formulas of taclets)
* that were modified after a certain point of time
- *
+ *
* Hashmaps of the particular lists of formulas; the keys of the maps is the point of time that
* separates old from new (modified) formulas
- *
+ *
* Keys: Long Values: IList
*/
public class IfInstantiationCachePool {
@@ -59,7 +59,7 @@ public void releaseAll() {
}
public void release(Node n) {
- IfInstantiationCache cache = null;
+ IfInstantiationCache cache;
synchronized (cacheMgr) {
cache = cacheMgr.remove(n);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java
index 2a01ee5fe2f..85ac05cca4d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java
@@ -195,9 +195,7 @@ protected static ImmutableList createInitialAppContainers(
for (RuleAppCost cost : costs) {
final TacletAppContainer container =
createContainer(p_app.head(), p_pio, p_goal, cost, true);
- if (container != null) {
- result = result.prepend(container);
- }
+ result = result.prepend(container);
p_app = p_app.tail();
}
return result;
@@ -244,13 +242,12 @@ protected boolean ifFormulasStillValid(Goal p_goal) {
while (it.hasNext()) {
final IfFormulaInstantiation ifInst2 = it.next();
- if (!(ifInst2 instanceof IfFormulaInstSeq))
+ if (!(ifInst2 instanceof final IfFormulaInstSeq ifInst))
// faster than assertTrue
{
- Debug.fail("Don't know what to do with the " + "if-instantiation " + ifInst2);
- }
- final IfFormulaInstSeq ifInst = (IfFormulaInstSeq) ifInst2;
- if (!(ifInst.inAntec() ? seq.antecedent() : seq.succedent())
+ Debug.fail("Don't know what to do with the " + "assumes-instantiation ", ifInst2);
+ throw new IllegalStateException("Unexpected assume-instantiation" + ifInst2);
+ } else if (!(ifInst.inAntec() ? seq.antecedent() : seq.succedent())
.contains(ifInst.getConstrainedFormula())) {
return false;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/TopRuleAppCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/TopRuleAppCost.java
index 0a4ffa5484e..ad0dc7c4b13 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/TopRuleAppCost.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/TopRuleAppCost.java
@@ -43,7 +43,7 @@ public final RuleAppCost add(@Nonnull RuleAppCost cost2) {
/**
* Multiply the TOP costs with given cost. TOP times any other costs results into TOP cost.
- *
+ *
* (weigl: Dicussable whether {@code TOP times 0 = 0}?)
*
* @param cost - non-null {@link RuleAppCost}
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
index f8e1ff45d96..cee112329ae 100644
--- 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
@@ -313,7 +313,7 @@ enum Candidate {
public boolean containsQuantifier;
/** one of CAND_* */
- public Candidate candidate;
+ private Candidate candidate;
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AppliedRuleAppsNameCache.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AppliedRuleAppsNameCache.java
index 68f80992584..ed1fdc8b7aa 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AppliedRuleAppsNameCache.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AppliedRuleAppsNameCache.java
@@ -95,7 +95,7 @@ public AppliedRuleAppsNameCache() {}
/**
* Gets rule apps applied to any node before the given node with the given name.
- *
+ *
* Multiple assumptions about nodes:
* * The given node is a leaf, no children, no applied rule
* * Only *new* nodes are appended to nodes
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsQuantifierFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsQuantifierFeature.java
index 7b71d6b9625..fda7af1fb88 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsQuantifierFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsQuantifierFeature.java
@@ -11,7 +11,7 @@
/**
* Binary feature that returns zero iff the focus of a rule contains a quantifier
- *
+ *
* NB: this can nowadays be done more nicely using term features
*/
public class ContainsQuantifierFeature extends AbstractBetaFeature {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsTermFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsTermFeature.java
index c3da0858c76..702831ef524 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsTermFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsTermFeature.java
@@ -32,11 +32,9 @@ public class ContainsTermFeature implements Feature {
/**
- * @param proj the ProjectionToTerm to the instantiation is supposed to be inspected
- * @param termFeature the term feature to use
- * @param noInstCost result if schemaVar
is not instantiated
- * @param demandInst if true
then raise an exception if schemaVar
is
- * not instantiated (otherwise: return noInstCost
)
+ * checks whether the second term is a subterm of the first one
+ * @param proj1 the ProjectionToTerm resolving to the term in which to search for the second term
+ * @param proj2 the ProjectionToTerm resolving to the term to be checked whether it is a subterm of the first one
*/
private ContainsTermFeature(ProjectionToTerm proj1, ProjectionToTerm proj2) {
this.proj1 = proj1;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DirectlyBelowFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DirectlyBelowFeature.java
index d4ad7fe2de6..8580119500a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DirectlyBelowFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DirectlyBelowFeature.java
@@ -13,7 +13,7 @@
* top-level and the symbol immediately above the focus is badSymbol
. Optionally, one
* can also specify that zero should only be returned if the symbol immediately above the focus is
* badSymbol
and the focus has a certain subterm index.
- *
+ *
* TODO: eliminate this class and use term features instead
*/
public abstract class DirectlyBelowFeature extends BinaryFeature {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DirectlyBelowSymbolFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DirectlyBelowSymbolFeature.java
index 1f2d7697909..ce11b4735ba 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DirectlyBelowSymbolFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DirectlyBelowSymbolFeature.java
@@ -10,7 +10,7 @@
* top-level and the symbol immediately above the focus is badSymbol
. Optionally, one
* can also specify that zero should only be returned if the symbol immediately above the focus is
* badSymbol
and the focus has a certain subterm index.
- *
+ *
* TODO: eliminate this class and use term features instead
*/
public class DirectlyBelowSymbolFeature extends DirectlyBelowFeature {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FindDepthFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FindDepthFeature.java
index a5d82eb7dc6..5658c13c825 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FindDepthFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FindDepthFeature.java
@@ -13,7 +13,7 @@
/**
* A feature that computes the depth of the find-position of a taclet (top-level positions have
* depth zero or if not a find taclet)
- *
+ *
* TODO: eliminate this class and use term features instead
*/
public class FindDepthFeature implements Feature {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java
index 12e912e6bfe..5a9fcbe306c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java
@@ -162,9 +162,7 @@ protected void collect(Term te, Services services) {
if (te.op() == add) {
collect(te.sub(0), services);
collect(te.sub(1), services);
- } else if (te.op() == Z) {
- // nothing
- } else {
+ } else if (te.op() != Z) {
addTerm(stripOffLiteral(te, services));
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ScaleFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ScaleFeature.java
index cae7c4a05e2..7771f4ff3f0 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ScaleFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ScaleFeature.java
@@ -126,10 +126,13 @@ public static Feature realAffine(Feature f, RuleAppCost dom0, RuleAppCost dom1,
* @param cost
*/
private static long getValue(RuleAppCost cost) {
- if (!(cost instanceof NumberRuleAppCost)) {
+ if (cost instanceof NumberRuleAppCost costValue) {
+ return costValue.getValue();
+ } else {
illegalCostError(cost);
+ // should never be reached
+ return 0;
}
- return ((NumberRuleAppCost) cost).getValue();
}
protected static void illegalCostError(final RuleAppCost cost) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TrivialMonomialLCRFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TrivialMonomialLCRFeature.java
index 022ffb8ea23..08c54f1a3f7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TrivialMonomialLCRFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TrivialMonomialLCRFeature.java
@@ -14,7 +14,7 @@
/**
* Return zero of the least common reducible of two monomials is so trivial that it is not necessary
* to do the critical pair completion
- *
+ *
* "A critical-pair/completion algorithm for finitely generated ideals in rings"
*/
public class TrivialMonomialLCRFeature extends BinaryTacletAppFeature {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java
index 6a3825548ea..7024e287652 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java
@@ -44,13 +44,11 @@ private int checkOperator(Operator op, int child, int pol) {
(op == Junctor.IMP && child == 0)) { // left hand side of implication
pol = pol * -1;
// do not change polarity if find term is subterm of
- } else if ((op == Junctor.AND) || // and
- (op == Junctor.OR) || // or
- (op == Junctor.IMP && child != 0) || // right hand side of implication
- (op == IfThenElse.IF_THEN_ELSE && child != 0)) { // then or else part of
+ } else if (!((op == Junctor.AND) || // and
+ (op == Junctor.OR) || // or
+ (op == Junctor.IMP && child != 0) || // right hand side of implication
+ (op == IfThenElse.IF_THEN_ELSE && child != 0))) { // then or else part of
// if-then-else
- // do nothing
- } else { // find term has no polarity in any other case
pol = 0;
}
return pol;
@@ -63,9 +61,6 @@ public boolean check(PosInOccurrence pio) {
final PIOPathIterator it = pio.iterator();
while (pol != 0 && it.next() != -1) {
pol = checkOperator(pio.subTerm().op(), it.getChild(), pol);
- if (pol == 0) {
- break;
- }
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/instantiator/SVInstantiationCP.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/instantiator/SVInstantiationCP.java
index 2d8b761e344..c0bfba287ea 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/instantiator/SVInstantiationCP.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/instantiator/SVInstantiationCP.java
@@ -93,11 +93,10 @@ private CP(RuleApp app, PosInOccurrence pos, Goal goal) {
}
public Iterator getBranches(RuleApp oldApp) {
- if (!(oldApp instanceof TacletApp)) {
- Debug.fail("Instantiation feature is only applicable to " + "taclet apps, but got "
- + oldApp);
+ if (!(oldApp instanceof final TacletApp tapp)) {
+ Debug.fail("Instantiation feature is only applicable to " + "taclet apps, but got ", oldApp);
+ throw new IllegalArgumentException("Rule application must be a taclet application, but is " + oldApp);
}
- final TacletApp tapp = (TacletApp) oldApp;
final SchemaVariable sv = findSVWithName(tapp);
final Term instTerm = value.toTerm(app, pos, goal);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java
index 81d379fdebb..4b933242c21 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java
@@ -533,7 +533,7 @@ private Constraint unifyHelp(Term t1, Term t2, boolean modifyThis, TermServices
/**
* checks for cycles and adds additional constraints if necessary
- *
+ *
* PRECONDITION: the sorts of mv and t match; if t is also a metavariable with same sort as mv,
* the order of mv and t is correct (using Metavariable.compareTo)
*
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java
index 4c48c4449f2..b06afcc0995 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java
@@ -8,6 +8,8 @@
import de.uka.ilkd.key.logic.op.ParsableVariable;
import de.uka.ilkd.key.logic.sort.Sort;
+import javax.annotation.Nonnull;
+
@Deprecated
public final class Metavariable extends AbstractSortedOperator
implements ParsableVariable, Comparable {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java
index 776025b320d..1631242a033 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java
@@ -246,7 +246,7 @@ private long firstRefine() {
private class Clause implements Iterable {
/** all literals contains in this clause */
- private ImmutableSet literals = DefaultImmutableSet.nil();
+ private ImmutableSet literals;
public Clause(ImmutableSet lits) {
literals = lits;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java
index e6efd4c7199..449c268a2f6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java
@@ -219,7 +219,7 @@ private boolean recAddTriggers(Term term, Services services) {
return true;
}
- return foundSubtriggers;
+ return true;
}
private Set expandIfThenElse(Term t, TermServices services) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TwoSidedMatching.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TwoSidedMatching.java
index a23d3d1bd35..39d1e0ecd84 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TwoSidedMatching.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TwoSidedMatching.java
@@ -17,10 +17,10 @@
/**
* Matching triggers within another quantifier expression. Problems with the current implementation:
- *
+ *
* * the usage of EqualityConstraint for unification implies that a variable is never instantiated
* with non-rigid terms
- *
+ *
* * it is unclear whether certain instantiations are lost due to too strict type checks in
* EqualityConstraint
*/
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/SVInstantiationProjection.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/SVInstantiationProjection.java
index f05a037c193..9b27c3dfec9 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/SVInstantiationProjection.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/SVInstantiationProjection.java
@@ -32,18 +32,17 @@ public static SVInstantiationProjection create(Name svName, boolean demandInst)
@Override
public Term toTerm(RuleApp app, PosInOccurrence pos, Goal goal) {
- if (!(app instanceof TacletApp)) {
+ if (!(app instanceof final TacletApp tapp)) {
Debug.fail("Projection is only applicable to taclet apps," + " but got " + app);
+ throw new IllegalArgumentException("Projections can only be applied to taclet applications, not to "+app);
}
-
- final TacletApp tapp = (TacletApp) app;
final Object instObj = tapp.instantiations().lookupValue(svName);
- if (!(instObj instanceof Term)) {
+ if (!(instObj instanceof Term instantiation)) {
Debug.assertFalse(demandInst, "Did not find schema variable " + svName
+ " that I was supposed to examine" + " (taclet " + tapp.taclet().name() + ")");
return null;
}
- return (Term) instObj;
+ return instantiation;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/TermConstructionProjection.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/TermConstructionProjection.java
index 0bcd1a4abe7..406e0ee9c48 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/TermConstructionProjection.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/TermConstructionProjection.java
@@ -13,7 +13,7 @@
/**
* Term projection for constructing a bigger term from a sequence of direct subterms and an
* operator.
- *
+ *
* NB: this is a rather restricted version of term construction, one can think of also allowing
* bound variables, etc to be specified
*/
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/EqTermFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/EqTermFeature.java
index 2d13f3c9027..357df4d57eb 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/EqTermFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/EqTermFeature.java
@@ -10,7 +10,7 @@
/**
* Term feature for testing equality of two terms. The feature returns zero iff it is invoked on a
* term that is equal to the current value of pattern
.
- *
+ *
* NB: it is not possible to use general ProjectionToTerm
here, because the information
* necessary to evaluate a ProjectionToTerm
is not available in a term feature
*/
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/IsInductionVariable.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/IsInductionVariable.java
index 0cbf1748a9b..48e3cf15c3d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/IsInductionVariable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/IsInductionVariable.java
@@ -10,7 +10,7 @@
/**
*
* The comment below was the description used in the variable condition:
- *
+ *
* In the taclet language the variable condition is called "\isInductVar". This variable
* condition checks if a logical variable is marked as an induction variable. A variable is marked
* as such if its name has the suffix is "Ind" or "IND" and the name has length>3.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/MultiplesModEquationsGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/MultiplesModEquationsGenerator.java
index af466c8a4e4..017b3735924 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/MultiplesModEquationsGenerator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/MultiplesModEquationsGenerator.java
@@ -33,7 +33,7 @@
* consisting of reduction steps with polynomials that have a single monomial. This is already
* enough to handle many practical cases and to significantly improve polynomial division modulo
* equations.
- *
+ *
* In the future, this class should also be used for instantiating explicit quantifiers over the
* integers.
*/
@@ -78,7 +78,7 @@ private Iterator toIterator(Term quotient) {
* Compute multiples of targetM
that are congruent to sourceM
modulo
* the polynomials in cofactorPolys
. The result is a list of terms x with the
* property x * targetM = sourceM (modulo ...)
.
- *
+ *
* This method will change the object cofactorPolys
.
*/
private ImmutableList computeMultiples(Monomial sourceM, Monomial targetM,
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
index b14de3dc315..acf16010282 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
@@ -383,8 +383,6 @@ public File saveProof(Proof proof, String fileExtension) {
try {
getMediator().stopInterface(true);
errorMsg = saver.save();
- } catch (IOException e) {
- errorMsg = e.toString();
} finally {
getMediator().startInterface(true);
}
@@ -414,15 +412,10 @@ public void saveProofBundle(Proof proof) {
Pair f = fileName(proof, ".zproof");
final int result = fileChooser.showSaveDialog(mainWindow, f.first, f.second);
if (result == JFileChooser.APPROVE_OPTION) {
- File file = fileChooser.getSelectedFile();
- ProofSaver saver = new ProofBundleSaver(proof, file);
+ final File file = fileChooser.getSelectedFile();
+ final ProofSaver saver = new ProofBundleSaver(proof, file);
+ final String errorMsg = saver.save();
- String errorMsg;
- try {
- errorMsg = saver.save();
- } catch (IOException e) {
- errorMsg = e.toString();
- }
if (errorMsg != null) {
mainWindow.notify(
new GeneralFailureEvent("Saving Proof failed.\n Error: " + errorMsg));
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java
index 160bf814369..0b6e22d8a0c 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java
@@ -54,17 +54,16 @@ public static void quickSave(MainWindow mainWindow) {
if (mainWindow.getMediator().ensureProofLoaded()) {
final String filename = QUICK_SAVE_PATH;
final Proof proof = mainWindow.getMediator().getSelectedProof();
- try {
- new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION).save();
- final String status = "File quicksaved: " + filename;
- mainWindow.setStatusLine(status);
- LOGGER.debug(status);
- } catch (IOException x) {
+ new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION).save();
+ final String status = "File quicksaved: " + filename;
+ if (status != null) {
mainWindow.popupWarning(
- "Quicksaving file " + filename + " failed:\n" + x.getMessage(),
- "Quicksave failed");
- LOGGER.debug("Quicksaving file {} failed.", filename, x);
+ "Quicksaving file " + filename + " failed:\n" + status,
+ "Quicksave failed");
+ LOGGER.debug("Quicksaving file {} failed.", filename, status);
}
+ mainWindow.setStatusLine(status);
+ LOGGER.debug(status);
} else {
mainWindow.popupWarning("No proof.", "Oops...");
}
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java
index 88ae96e15c8..8673693c7f9 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java
@@ -218,11 +218,7 @@ private void saveSideProof(Proof proof) {
final File toSave = new File(proofFolder, filename);
final KeYResourceManager krm = KeYResourceManager.getManager();
final ProofSaver ps = new ProofSaver(proof, toSave.getAbsolutePath(), krm.getSHA1());
- try {
- ps.save();
- } catch (IOException e) {
- reportException(this, null, e);
- }
+ ps.save();
}
/**
From 53b4c673bf26639c5e21c76029484ea7855e013b Mon Sep 17 00:00:00 2001
From: Richard Bubel
Date: Wed, 4 Oct 2023 21:50:05 +0200
Subject: [PATCH 2/5] spotless fixes
---
.../key/proof/SVInstantiationExceptionWithPosition.java | 1 -
.../uka/ilkd/key/proof/io/consistency/MemoryFileRepo.java | 1 -
.../main/java/de/uka/ilkd/key/prover/StopCondition.java | 2 +-
.../ilkd/key/prover/impl/SingleRuleApplicationInfo.java | 2 +-
.../ilkd/key/strategy/feature/ContainsTermFeature.java | 7 +++++--
.../feature/findprefix/AntecSuccPrefixChecker.java | 8 ++++----
.../strategy/feature/instantiator/SVInstantiationCP.java | 6 ++++--
.../key/strategy/quantifierHeuristics/Metavariable.java | 1 -
.../termProjection/SVInstantiationProjection.java | 3 ++-
.../de/uka/ilkd/key/gui/WindowUserInterfaceControl.java | 1 -
.../java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java | 5 ++---
.../ilkd/key/ui/AbstractMediatorUserInterfaceControl.java | 1 -
12 files changed, 19 insertions(+), 19 deletions(-)
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java b/key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java
index 023713557bd..2de88e1ddd3 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java
@@ -4,7 +4,6 @@
package de.uka.ilkd.key.proof;
-import java.net.MalformedURLException;
import javax.annotation.Nullable;
import de.uka.ilkd.key.java.Position;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/MemoryFileRepo.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/MemoryFileRepo.java
index f735f856497..ea5d7af5453 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/MemoryFileRepo.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/MemoryFileRepo.java
@@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof.io.consistency;
-import java.io.IOException;
import java.io.InputStream;
import java.io.OutputStream;
import java.net.URL;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/StopCondition.java b/key.core/src/main/java/de/uka/ilkd/key/prover/StopCondition.java
index f28599cc582..7ddb2ad2c1c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/prover/StopCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/prover/StopCondition.java
@@ -71,7 +71,7 @@ boolean isGoalAllowed(int maxApplications, long timeout, Proof proof, long start
/**
* Returns the reason why the previous check via
- * {@link #isGoalAllowed(int, long, Proof, long, int, Goal)} has
+ * {@link #isGoalAllowed(int, long, Proof, long, int, Goal)} has
* stopped the apply strategy.
*
* @param maxApplications The defined maximal number of rules to apply. Can be different to
diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/SingleRuleApplicationInfo.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/SingleRuleApplicationInfo.java
index 6f9fc4f0468..2c29c1ef7fb 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/SingleRuleApplicationInfo.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/SingleRuleApplicationInfo.java
@@ -8,7 +8,7 @@
/**
* Instances of this class are used to store if a rule could be applied automatically and if not to
- * store the reason why no rule applications could be performed.
+ * store the reason why no rule applications could be performed.
*/
public class SingleRuleApplicationInfo {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsTermFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsTermFeature.java
index 702831ef524..d93de743e25 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsTermFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsTermFeature.java
@@ -33,8 +33,11 @@ public class ContainsTermFeature implements Feature {
/**
* checks whether the second term is a subterm of the first one
- * @param proj1 the ProjectionToTerm resolving to the term in which to search for the second term
- * @param proj2 the ProjectionToTerm resolving to the term to be checked whether it is a subterm of the first one
+ *
+ * @param proj1 the ProjectionToTerm resolving to the term in which to search for the second
+ * term
+ * @param proj2 the ProjectionToTerm resolving to the term to be checked whether it is a subterm
+ * of the first one
*/
private ContainsTermFeature(ProjectionToTerm proj1, ProjectionToTerm proj2) {
this.proj1 = proj1;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java
index 7024e287652..92405017d8f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/findprefix/AntecSuccPrefixChecker.java
@@ -45,10 +45,10 @@ private int checkOperator(Operator op, int child, int pol) {
pol = pol * -1;
// do not change polarity if find term is subterm of
} else if (!((op == Junctor.AND) || // and
- (op == Junctor.OR) || // or
- (op == Junctor.IMP && child != 0) || // right hand side of implication
- (op == IfThenElse.IF_THEN_ELSE && child != 0))) { // then or else part of
- // if-then-else
+ (op == Junctor.OR) || // or
+ (op == Junctor.IMP && child != 0) || // right hand side of implication
+ (op == IfThenElse.IF_THEN_ELSE && child != 0))) { // then or else part of
+ // if-then-else
pol = 0;
}
return pol;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/instantiator/SVInstantiationCP.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/instantiator/SVInstantiationCP.java
index c0bfba287ea..9d7c2741e38 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/instantiator/SVInstantiationCP.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/instantiator/SVInstantiationCP.java
@@ -94,8 +94,10 @@ private CP(RuleApp app, PosInOccurrence pos, Goal goal) {
public Iterator getBranches(RuleApp oldApp) {
if (!(oldApp instanceof final TacletApp tapp)) {
- Debug.fail("Instantiation feature is only applicable to " + "taclet apps, but got ", oldApp);
- throw new IllegalArgumentException("Rule application must be a taclet application, but is " + oldApp);
+ Debug.fail("Instantiation feature is only applicable to " + "taclet apps, but got ",
+ oldApp);
+ throw new IllegalArgumentException(
+ "Rule application must be a taclet application, but is " + oldApp);
}
final SchemaVariable sv = findSVWithName(tapp);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java
index b06afcc0995..9cdbea235e6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Metavariable.java
@@ -8,7 +8,6 @@
import de.uka.ilkd.key.logic.op.ParsableVariable;
import de.uka.ilkd.key.logic.sort.Sort;
-import javax.annotation.Nonnull;
@Deprecated
public final class Metavariable extends AbstractSortedOperator
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/SVInstantiationProjection.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/SVInstantiationProjection.java
index 9b27c3dfec9..29bd3024f67 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/SVInstantiationProjection.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/SVInstantiationProjection.java
@@ -34,7 +34,8 @@ public static SVInstantiationProjection create(Name svName, boolean demandInst)
public Term toTerm(RuleApp app, PosInOccurrence pos, Goal goal) {
if (!(app instanceof final TacletApp tapp)) {
Debug.fail("Projection is only applicable to taclet apps," + " but got " + app);
- throw new IllegalArgumentException("Projections can only be applied to taclet applications, not to "+app);
+ throw new IllegalArgumentException(
+ "Projections can only be applied to taclet applications, not to " + app);
}
final Object instObj = tapp.instantiations().lookupValue(svName);
if (!(instObj instanceof Term instantiation)) {
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
index acf16010282..da191a6b8fc 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
@@ -4,7 +4,6 @@
package de.uka.ilkd.key.gui;
import java.io.File;
-import java.io.IOException;
import java.util.Collection;
import java.util.LinkedList;
import java.util.List;
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java
index 0b6e22d8a0c..ffe1f20531c 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java
@@ -5,7 +5,6 @@
import java.awt.event.ActionEvent;
import java.io.File;
-import java.io.IOException;
import de.uka.ilkd.key.gui.MainWindow;
import de.uka.ilkd.key.proof.Proof;
@@ -58,8 +57,8 @@ public static void quickSave(MainWindow mainWindow) {
final String status = "File quicksaved: " + filename;
if (status != null) {
mainWindow.popupWarning(
- "Quicksaving file " + filename + " failed:\n" + status,
- "Quicksave failed");
+ "Quicksaving file " + filename + " failed:\n" + status,
+ "Quicksave failed");
LOGGER.debug("Quicksaving file {} failed.", filename, status);
}
mainWindow.setStatusLine(status);
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java
index 8673693c7f9..0a0002e67d0 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java
@@ -4,7 +4,6 @@
package de.uka.ilkd.key.ui;
import java.io.File;
-import java.io.IOException;
import java.util.List;
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
From 826eb61ed77d0002fa3904f9eecf1a2354ed0af1 Mon Sep 17 00:00:00 2001
From: Richard Bubel
Date: Wed, 4 Oct 2023 22:06:12 +0200
Subject: [PATCH 3/5] Fix error behavior during proof saving
---
.../ilkd/key/ui/AbstractMediatorUserInterfaceControl.java | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java
index 0a0002e67d0..05becc26ca9 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java
@@ -4,6 +4,7 @@
package de.uka.ilkd.key.ui;
import java.io.File;
+import java.io.IOException;
import java.util.List;
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
@@ -217,7 +218,10 @@ private void saveSideProof(Proof proof) {
final File toSave = new File(proofFolder, filename);
final KeYResourceManager krm = KeYResourceManager.getManager();
final ProofSaver ps = new ProofSaver(proof, toSave.getAbsolutePath(), krm.getSHA1());
- ps.save();
+ final String errorMsg = ps.save();
+ if (errorMsg != null) {
+ reportException(this, null, new IOException(errorMsg));
+ }
}
/**
From 783c430b93f4651e9e8eb467229c4caaf2022ad9 Mon Sep 17 00:00:00 2001
From: Richard Bubel
Date: Fri, 13 Oct 2023 11:17:58 +0200
Subject: [PATCH 4/5] Remove invalid JavaDoc refering to not thrown exceptions
---
.../java/de/uka/ilkd/key/proof/init/DependencyContractPO.java | 2 --
.../de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java | 2 --
.../java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java | 1 -
key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java | 3 ---
key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java | 4 ++--
5 files changed, 2 insertions(+), 10 deletions(-)
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
index 616c51e7d7e..2c69a146c30 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
@@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof.init;
-import java.io.IOException;
import java.util.*;
import de.uka.ilkd.key.java.Services;
@@ -302,7 +301,6 @@ public void fillSaveProperties(Properties properties) {
* @param initConfig The already load {@link InitConfig}.
* @param properties The settings of the proof obligation to instantiate.
* @return The instantiated proof obligation.
- * @throws IOException Occurred Exception.
*/
public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
String contractName = properties.getProperty("contract");
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
index 9d47742b614..eade4cca4c6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
@@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof.init;
-import java.io.IOException;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
@@ -80,7 +79,6 @@ public FunctionalLoopContractPO(InitConfig initConfig, FunctionalLoopContract co
* @param initConfig The already load {@link InitConfig}.
* @param properties The settings of the proof obligation to instantiate.
* @return The instantiated proof obligation.
- * @throws IOException Occurred Exception.
*/
public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
String contractName = properties.getProperty("contract");
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
index 6e9072ec1ff..455491c16ff 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
@@ -240,7 +240,6 @@ public Profile getProfile() {
*
* @return The {@link Profile} defined by the file to load or {@code null} if no {@link Profile}
* is defined by the file.
- * @throws Exception Occurred Exception.
*/
private Profile readProfileFromFile() {
@Nonnull
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java
index f92d19995fa..f806dd2221c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java
@@ -58,7 +58,6 @@ public interface EnvInput {
return null;
}
-
/**
* gets the classpath elements to be considered here.
*/
@@ -67,8 +66,6 @@ public interface EnvInput {
/**
* gets the boot classpath element, null if none set.
- *
- * @throws
*/
File readBootClassPath();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java
index 4013351ffbf..77c442f7469 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java
@@ -39,7 +39,8 @@ public interface LDTInputListener {
* creates a representation of the LDT files to be used as input to the KeY prover.
*
* @param keyFiles an array containing the LDT .key files
- * @param main the main class used to report the progress of reading
+ * @param listener an LDTInputListener for stsus reports while loading
+ * @param profile the Profile for which the LDTs are load
*/
public LDTInput(KeYFile[] keyFiles, LDTInputListener listener, Profile profile) {
assert profile != null;
@@ -162,7 +163,6 @@ public boolean equals(Object o) {
return true;
}
-
@Override
public int hashCode() {
int result = 0;
From 337b74583f2b8cf503f50f639fb549b837473fc2 Mon Sep 17 00:00:00 2001
From: Alexander Weigl
Date: Fri, 13 Oct 2023 09:21:52 +0000
Subject: [PATCH 5/5] JavaDoc @throws fixes
---
.../uka/ilkd/key/proof/init/DependencyContractPO.java | 2 --
.../key/proof/init/FunctionalBlockContractPO.java | 2 --
.../ilkd/key/proof/init/FunctionalLoopContractPO.java | 2 --
.../uka/ilkd/key/proof/init/KeYUserProblemFile.java | 1 -
.../de/uka/ilkd/key/proof/init/WellDefinednessPO.java | 2 --
.../main/java/de/uka/ilkd/key/proof/io/EnvInput.java | 2 --
.../de/uka/ilkd/key/gui/actions/QuickSaveAction.java | 11 +++++------
7 files changed, 5 insertions(+), 17 deletions(-)
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
index 616c51e7d7e..2c69a146c30 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
@@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof.init;
-import java.io.IOException;
import java.util.*;
import de.uka.ilkd.key.java.Services;
@@ -302,7 +301,6 @@ public void fillSaveProperties(Properties properties) {
* @param initConfig The already load {@link InitConfig}.
* @param properties The settings of the proof obligation to instantiate.
* @return The instantiated proof obligation.
- * @throws IOException Occurred Exception.
*/
public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
String contractName = properties.getProperty("contract");
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
index 5e3fe8fba23..62c580484bf 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
@@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof.init;
-import java.io.IOException;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
@@ -80,7 +79,6 @@ public FunctionalBlockContractPO(InitConfig initConfig, FunctionalBlockContract
* @param initConfig The already load {@link InitConfig}.
* @param properties The settings of the proof obligation to instantiate.
* @return The instantiated proof obligation.
- * @throws IOException Occurred Exception.
*/
public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
String contractName = properties.getProperty("contract");
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
index 9d47742b614..eade4cca4c6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
@@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof.init;
-import java.io.IOException;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
@@ -80,7 +79,6 @@ public FunctionalLoopContractPO(InitConfig initConfig, FunctionalLoopContract co
* @param initConfig The already load {@link InitConfig}.
* @param properties The settings of the proof obligation to instantiate.
* @return The instantiated proof obligation.
- * @throws IOException Occurred Exception.
*/
public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
String contractName = properties.getProperty("contract");
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
index 6e9072ec1ff..455491c16ff 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
@@ -240,7 +240,6 @@ public Profile getProfile() {
*
* @return The {@link Profile} defined by the file to load or {@code null} if no {@link Profile}
* is defined by the file.
- * @throws Exception Occurred Exception.
*/
private Profile readProfileFromFile() {
@Nonnull
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
index 4a37555543e..4bf418301d7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
@@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof.init;
-import java.io.IOException;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Properties;
@@ -299,7 +298,6 @@ public void fillSaveProperties(Properties properties) {
* @param initConfig The already load {@link InitConfig}.
* @param properties The settings of the proof obligation to instantiate.
* @return The instantiated proof obligation.
- * @throws IOException Occurred Exception.
*/
public static LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties) {
String contractName = properties.getProperty("wd check");
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java
index f92d19995fa..b1aaf1ddb5c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java
@@ -67,8 +67,6 @@ public interface EnvInput {
/**
* gets the boot classpath element, null if none set.
- *
- * @throws
*/
File readBootClassPath();
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java
index ffe1f20531c..8baa2212175 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java
@@ -55,12 +55,11 @@ public static void quickSave(MainWindow mainWindow) {
final Proof proof = mainWindow.getMediator().getSelectedProof();
new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION).save();
final String status = "File quicksaved: " + filename;
- if (status != null) {
- mainWindow.popupWarning(
- "Quicksaving file " + filename + " failed:\n" + status,
- "Quicksave failed");
- LOGGER.debug("Quicksaving file {} failed.", filename, status);
- }
+ mainWindow.popupWarning(
+ "Quicksaving file " + filename + " failed:\n" + status,
+ "Quicksave failed");
+ LOGGER.debug("Quicksaving file {} failed.", filename, status);
+
mainWindow.setStatusLine(status);
LOGGER.debug(status);
} else {