diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index a3bd4d9a1b2..c3aecbc0256 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -9,6 +9,22 @@ on: - 'KeY-*' jobs: + checkerFramework: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v3 + - name: Set up JDK 21 + uses: actions/setup-java@v3 + with: + java-version: 21 + distribution: 'corretto' + cache: 'gradle' + - name: Build with Gradle + uses: gradle/gradle-build-action@v2.4.2 + with: + arguments: -DENABLE_NULLNESS=true compileTest + + qodana: runs-on: ubuntu-latest steps: diff --git a/build.gradle b/build.gradle index 5bb1ef3456b..31395c205f8 100644 --- a/build.gradle +++ b/build.gradle @@ -22,6 +22,9 @@ plugins { // Code formatting id "com.diffplug.spotless" version "6.25.0" + + // EISOP Checker Framework + id "org.checkerframework" version "0.6.28" } // Configure this project for use inside IntelliJ: @@ -53,6 +56,7 @@ subprojects { apply plugin: "com.diffplug.spotless" apply plugin: "checkstyle" apply plugin: "pmd" + apply plugin: "org.checkerframework" group = rootProject.group version = rootProject.version @@ -71,6 +75,19 @@ subprojects { dependencies { implementation("org.slf4j:slf4j-api:2.0.13") + implementation("org.slf4j:slf4j-api:2.0.12") + testImplementation("ch.qos.logback:logback-classic:1.4.8") + + //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0' + //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0' + + compileOnly("org.jspecify:jspecify:0.3.0") + testCompileOnly("org.jspecify:jspecify:0.3.0") + def eisop_version = "3.42.0-eisop2" + compileOnly "io.github.eisop:checker-qual:$eisop_version" + compileOnly "io.github.eisop:checker-util:$eisop_version" + testCompileOnly "io.github.eisop:checker-qual:$eisop_version" + checkerFramework "io.github.eisop:checker:$eisop_version" testImplementation("ch.qos.logback:logback-classic:1.5.6") testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.2' @@ -80,8 +97,6 @@ subprojects { testCompileOnly 'junit:junit:4.13.2' testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.2' testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2' - - implementation("org.jspecify:jspecify:0.3.0") } tasks.withType(JavaCompile) { @@ -346,6 +361,19 @@ subprojects { } } +// checkerFramework { +// checkers = [ +// "org.checkerframework.checker.nullness.NullnessChecker", +// ] +// extraJavacArgs = [ +// "-AonlyDefs=^org\\.key_project\\.util", +// "-Xmaxerrs", "10000", +// "-Astubs=$projectDir/src/main/checkerframework", +// "-Werror", +// "-Aversion", +// ] +// } + afterEvaluate { // required so project.description is non-null as set by sub build.gradle publishing { publications { diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java index 8773f536ec1..f55f6111dcc 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java @@ -384,7 +384,7 @@ public static boolean containsSequentFormulasToRefactor(TermLabelState state) { @SuppressWarnings("unchecked") Set sfSet = (Set) labelState.get(SEQUENT_FORMULA_REFACTORING_REQUIRED); - return !CollectionUtil.isEmpty(sfSet); + return sfSet != null && !sfSet.isEmpty(); } /** 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 0be6244d625..785b03e3d80 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 @@ -4141,7 +4141,7 @@ public static boolean lazyComputeIsAdditionalBranchVerified(Node node) { Set additinalPredicates = AbstractOperationPO.getAdditionalUninterpretedPredicates(node.proof()); // Check if node can be treated as verified/closed - if (!CollectionUtil.isEmpty(additinalPredicates)) { + if (additinalPredicates != null && !additinalPredicates.isEmpty()) { boolean verified = true; Iterator leafsIter = node.leavesIterator(); while (verified && leafsIter.hasNext()) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java index a7b80f23363..65d08de9837 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java @@ -55,7 +55,7 @@ public String getDescription() { @Override public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { - if (goals == null || goals.head() == null || goals.head().node() == null + if (goals == null || goals.isEmpty() || goals.head().node() == null || goals.head().node().parent() == null) { return false; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java index cd9f38083b4..e37ab3aefe9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java @@ -51,7 +51,7 @@ public String getDescription() { @Override public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { - if (goals == null || goals.head() == null || goals.head().node() == null + if (goals == null || goals.isEmpty() || goals.head().node() == null || goals.head().node().parent() == null) { return false; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java index 33dc44f19d0..c04e45bebe2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java @@ -52,7 +52,7 @@ public String getDescription() { @Override public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { - if (goals == null || goals.head() == null) { + if (goals == null || goals.isEmpty()) { return false; } if (posInOcc == null || posInOcc.subTerm() == null) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.java index 217093da97a..dc0912874df 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.java @@ -66,7 +66,12 @@ private void linkSymbExecVarsToCopies() { private void linkStateVarsToCopies(StateVars ifVars, StateVars seVars, Map map) { final Iterator ifVarsIt = ifVars.termList.iterator(); for (final Term symbTerm : seVars.termList) { - final Term ifTerm = ifVarsIt.next(); + final Term ifTerm; + if (ifVarsIt.hasNext()) { + ifTerm = ifVarsIt.next(); + } else { + ifTerm = null; + } if (symbTerm != null) { map.put(symbTerm, ifTerm); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java index 3e03d7b704c..3df934302d5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java @@ -1061,7 +1061,9 @@ public ProgramVariable getAttribute(final String attributeName, Sort s) { */ public ProgramVariable getCanonicalFieldProgramVariable(String fieldName, KeYJavaType kjt) { ImmutableList allAttributes = getAllAttributes(fieldName, kjt, false); - if (kjt.getJavaType() instanceof ArrayType) { + if (allAttributes.isEmpty()) { + return null; + } else if (kjt.getJavaType() instanceof ArrayType) { return allAttributes.head(); } else { return allAttributes.reverse().head(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Choice.java b/key.core/src/main/java/de/uka/ilkd/key/logic/Choice.java index b9efbd2dcb4..56ba6bdd40e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/Choice.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/Choice.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.logic; - import java.util.List; import java.util.Objects; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java index e995affe6a5..4606c6fd57f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java @@ -24,6 +24,7 @@ import org.antlr.v4.runtime.misc.ParseCancellationException; import org.antlr.v4.runtime.tree.TerminalNode; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -37,6 +38,7 @@ * @author Alexander Weigl * @version 1 (19.08.19) */ +@NullMarked public final class ParsingFacade { private static final Logger LOGGER = LoggerFactory.getLogger(ParsingFacade.class); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java index 01d1b37b512..048588c7717 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java @@ -22,8 +22,8 @@ import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.sort.Sort; -import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; +import org.key_project.util.collection.Immutables; import org.antlr.v4.runtime.Token; import org.slf4j.Logger; @@ -147,9 +147,9 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { Name sortName = new Name(sortId); ImmutableSet ext = sortExt == null ? ImmutableSet.empty() - : DefaultImmutableSet.fromCollection(sortExt); + : Immutables.createSetFrom(sortExt); ImmutableSet oneOf = sortOneOf == null ? ImmutableSet.empty() - : DefaultImmutableSet.fromCollection(sortOneOf); + : Immutables.createSetFrom(sortOneOf); // attention: no expand to java.lang here! Sort existingSort = sorts().lookup(sortName); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index a80a85e8728..a2930cd98cc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -27,11 +27,7 @@ import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; -import org.key_project.util.collection.DefaultImmutableSet; -import org.key_project.util.collection.ImmutableList; -import org.key_project.util.collection.ImmutableSLList; -import org.key_project.util.collection.ImmutableSet; -import org.key_project.util.collection.Pair; +import org.key_project.util.collection.*; import antlr.RecognitionException; import org.antlr.v4.runtime.ParserRuleContext; @@ -740,7 +736,7 @@ public Object visitAddrules(KeYParser.AddrulesContext ctx) { @Override public ImmutableSet visitAddprogvar(KeYParser.AddprogvarContext ctx) { final Collection accept = accept(ctx.pvs); - return ImmutableSet.fromSet(new HashSet<>(Objects.requireNonNull(accept))); + return Immutables.createSetFrom(Objects.requireNonNull(accept)); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/ParserException.java b/key.core/src/main/java/de/uka/ilkd/key/parser/ParserException.java index 0de46fa6f2b..ec53ac9dcb7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/parser/ParserException.java +++ b/key.core/src/main/java/de/uka/ilkd/key/parser/ParserException.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.parser; - import de.uka.ilkd.key.util.parsing.HasLocation; import org.jspecify.annotations.Nullable; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java index 0a1080a1a3b..3ab62baf095 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java @@ -37,6 +37,7 @@ import org.key_project.util.lookup.Lookup; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; import org.jspecify.annotations.Nullable; @@ -49,6 +50,7 @@ * information, and methods to apply rules. Furthermore, it offers services that deliver the open * goals, namespaces and several other information about the current state of the proof. */ +@NullMarked public class Proof implements Named { /** @@ -56,10 +58,14 @@ public class Proof implements Named { */ final long creationTime = System.currentTimeMillis(); - /** name of the proof */ + /** + * name of the proof + */ private final Name name; - /** the root of the proof */ + /** + * the root of the proof + */ private Node root; /** @@ -68,7 +74,9 @@ public class Proof implements Named { */ private final List listenerList = new LinkedList<>(); - /** list with the open goals of the proof */ + /** + * list with the open goals of the proof + */ private ImmutableList openGoals = ImmutableSLList.nil(); /** @@ -78,22 +86,35 @@ public class Proof implements Named { */ private ImmutableList closedGoals = ImmutableSLList.nil(); - /** declarations &c, read from a problem file or otherwise */ + /** + * declarations &c, read from a problem file or otherwise + */ private String problemHeader = ""; - /** the proof environment (optional) */ + /** + * the proof environment (optional) + */ + @Nullable private ProofEnvironment env; - /** maps the Abbreviations valid for this proof to their corresponding terms. */ + /** + * maps the Abbreviations valid for this proof to their corresponding terms. + */ private AbbrevMap abbreviations = new AbbrevMap(); - /** the logic configuration for this proof, i.e., logic signature, rules etc. */ + /** + * the logic configuration for this proof, i.e., logic signature, rules etc. + */ private InitConfig initConfig; - /** the environment of the proof with specs and java model */ + /** + * the environment of the proof with specs and java model + */ private ProofCorrectnessMgt localMgt; - /** settings valid independent of a proof */ + /** + * settings valid independent of a proof + */ private final ProofIndependentSettings pis; /** * when different users load and save a proof this vector fills up with Strings containing the @@ -109,6 +130,7 @@ public class Proof implements Named { private long autoModeTime = 0; + @Nullable private Strategy activeStrategy; private PropertyChangeListener settingsListener; @@ -119,7 +141,9 @@ public class Proof implements Named { */ private boolean disposed = false; - /** list of rule app listeners */ + /** + * list of rule app listeners + */ private final List ruleAppListenerList = Collections.synchronizedList(new ArrayList<>(10)); /** @@ -131,6 +155,7 @@ public class Proof implements Named { * The {@link File} under which this {@link Proof} was saved the last time if available or * {@code null} otherwise. */ + @Nullable private File proofFile; @Nullable @@ -188,8 +213,9 @@ private void initStrategy() { } - - /** constructs a new empty proof with name */ + /** + * constructs a new empty proof with name + */ public Proof(String name, InitConfig initConfig) { this(new Name(name), initConfig); } @@ -199,7 +225,6 @@ private Proof(String name, Sequent problem, TacletIndex rules, BuiltInRuleIndex this(new Name(name), initConfig); final var rootNode = new Node(this, problem); - final var firstGoal = new Goal(rootNode, rules, new BuiltInRuleAppIndex(builtInRules), getServices()); openGoals = openGoals.prepend(firstGoal); @@ -251,7 +276,7 @@ public void dispose() { } if (localMgt != null) { localMgt.removeProofListener(); // This is strongly required because the listener is - // contained in a static List + // contained in a static List } // remove setting listener from settings initConfig.getSettings().getStrategySettings() @@ -312,12 +337,16 @@ public NamespaceSet getNamespaces() { return getServices().getNamespaces(); } - /** returns the JavaInfo with the java type information */ + /** + * returns the JavaInfo with the java type information + */ public JavaInfo getJavaInfo() { return getServices().getJavaInfo(); } - /** returns the Services with the java service classes */ + /** + * returns the Services with the java service classes + */ public Services getServices() { return initConfig.getServices(); } @@ -331,8 +360,9 @@ public void addAutoModeTime(long time) { } - - /** sets the variable, function, sort, heuristics namespaces */ + /** + * sets the variable, function, sort, heuristics namespaces + */ public void setNamespaces(NamespaceSet ns) { getServices().setNamespaces(ns); if (!root.leaf()) { @@ -401,7 +431,9 @@ public Node root() { } - /** sets the root of the proof */ + /** + * sets the root of the proof + */ public void setRoot(Node root) { if (this.root != null) { throw new IllegalStateException("Tried to reset the root of the proof."); @@ -444,7 +476,6 @@ public ImmutableList closedGoals() { * Returns the list of all, open and closed, goals. * * @return list with all goals. - * * @see #openGoals() * @see #closedGoals() */ @@ -469,8 +500,8 @@ public ImmutableList openEnabledGoals() { * * @param goals non-null list of goals * @return sublist such that every goal in the list is enabled - * @see Goal#isAutomatic() * @author mulbrich + * @see Goal#isAutomatic() */ private ImmutableList filterEnabledGoals(ImmutableList goals) { ImmutableList enabledGoals = ImmutableSLList.nil(); @@ -536,8 +567,8 @@ public void closeGoal(Goal goalToClose) { /** * Opens a previously closed node (the one corresponding to p_goal) and all its closed parents. - *

* + *

* This is, for instance, needed for the {@code MergeRule}: In a situation where a merge node * and its associated partners have been closed and the merge node is then pruned away, the * partners have to be reopened again. Otherwise, we have a soundness issue. @@ -748,7 +779,9 @@ public void traverseFromChildToParent(Node child, Node parent, ProofVisitor visi } while (child != parent); } - /** fires the event that the proof has been expanded at the given node */ + /** + * fires the event that the proof has been expanded at the given node + */ public void fireProofExpanded(Node node) { ProofTreeEvent e = new ProofTreeEvent(this, node); synchronized (listenerList) { @@ -758,7 +791,9 @@ public void fireProofExpanded(Node node) { } } - /** fires the event that the proof is being pruned at the given node */ + /** + * fires the event that the proof is being pruned at the given node + */ protected void fireProofIsBeingPruned(Node below) { ProofTreeEvent e = new ProofTreeEvent(this, below); synchronized (listenerList) { @@ -768,7 +803,9 @@ protected void fireProofIsBeingPruned(Node below) { } } - /** fires the event that the proof has been pruned at the given node */ + /** + * fires the event that the proof has been pruned at the given node + */ protected void fireProofPruned(Node below) { ProofTreeEvent e = new ProofTreeEvent(this, below); synchronized (listenerList) { @@ -779,7 +816,9 @@ protected void fireProofPruned(Node below) { } - /** fires the event that the proof has been restructured */ + /** + * fires the event that the proof has been restructured + */ public void fireProofStructureChanged() { ProofTreeEvent e = new ProofTreeEvent(this); synchronized (listenerList) { @@ -790,7 +829,9 @@ public void fireProofStructureChanged() { } - /** fires the event that a goal has been removed from the list of goals */ + /** + * fires the event that a goal has been removed from the list of goals + */ protected void fireProofGoalRemoved(Goal goal) { ProofTreeEvent e = new ProofTreeEvent(this, goal); synchronized (listenerList) { @@ -822,7 +863,9 @@ protected void fireProofGoalsAdded(Goal goal) { } - /** fires the event that the proof has been restructured */ + /** + * fires the event that the proof has been restructured + */ public void fireProofGoalsChanged() { ProofTreeEvent e = new ProofTreeEvent(this, openGoals()); synchronized (listenerList) { @@ -1051,7 +1094,9 @@ public Statistics getStatistics() { return new Statistics(this); } - /** toString */ + /** + * toString + */ @Override public String toString() { StringBuilder result = new StringBuilder(); @@ -1070,7 +1115,9 @@ public String toString() { return result.toString(); } - /** fires the event that a rule has been applied */ + /** + * fires the event that a rule has been applied + */ protected void fireRuleApplied(ProofEvent p_e) { synchronized (ruleAppListenerList) { for (RuleAppListener ral : ruleAppListenerList) { @@ -1188,7 +1235,6 @@ public void setProofFile(File proofFile) { } /** - * * @return the current profile's factory for the active strategy, or the default factory if * there is no active strategy. * @see Profile#getStrategyFactory(Name) 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 d717309e744..5999035fb84 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 @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof; - import java.net.MalformedURLException; import de.uka.ilkd.key.java.Position; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java index 4ac93a95db9..dec35658527 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java @@ -35,6 +35,7 @@ import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; +import org.key_project.util.collection.Immutables; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; @@ -333,8 +334,8 @@ public ImmutableSet readContracts() { ContractsAndInvariantsFinder cinvs = new ContractsAndInvariantsFinder(initConfig.getServices(), initConfig.namespaces()); getParseContext().accept(cinvs); - specRepos.addContracts(ImmutableSet.fromCollection(cinvs.getContracts())); - specRepos.addClassInvariants(ImmutableSet.fromCollection(cinvs.getInvariants())); + specRepos.addContracts(Immutables.createSetFrom(cinvs.getContracts())); + specRepos.addClassInvariants(Immutables.createSetFrom(cinvs.getInvariants())); return DefaultImmutableSet.nil(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java index 400e8b62266..4cb5be62e48 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/package-info.java @@ -3,4 +3,7 @@ * example, proof management ensures that contract applications cannot lead to * unsound cyclic dependencies between proofs. */ +@NullMarked package de.uka.ilkd.key.proof.mgt; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java index 646e10b2547..8c505c74360 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule; - import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.proof.Goal; 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 d930c46b70f..2d3ca83afb4 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 @@ -494,11 +494,12 @@ public boolean equalsModProofIrrelevancy(Object o) { } else { ImmutableList if1 = ifSequent.asList(); ImmutableList if2 = t2.ifSequent.asList(); - while (if1.head() != null && if1.head().equalsModProofIrrelevancy(if2.head())) { + while (!if1.isEmpty() && !if2.isEmpty() + && if1.head().equalsModProofIrrelevancy(if2.head())) { if1 = if1.tail(); if2 = if2.tail(); } - if (if1.head() != null || if2.head() != null) { + if (!if1.isEmpty() || !if2.isEmpty()) { return false; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLDepends.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLDepends.java index 679742eeeef..a1ae32e4d86 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLDepends.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLDepends.java @@ -15,7 +15,6 @@ import org.jspecify.annotations.NonNull; - /** * A JML depends / accessible clause for a model field in textual form. Note that such clauses for * *methods* are part of TextualJMLSpecCase. diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMergePointDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMergePointDecl.java index 8e9a0eaa90c..3670536c07b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMergePointDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMergePointDecl.java @@ -9,26 +9,29 @@ import org.key_project.util.collection.ImmutableList; -import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; + /** * A JML merge point declaration in textual form. - * + *

* TODO: Adapt this to the specific needs of merge point declarations. * * @author Dominic Scheurer */ +@NullMarked public final class TextualJMLMergePointDecl extends TextualJMLConstruct { - private final JmlParser.@NonNull Merge_point_statementContext mergeProc; - public TextualJMLMergePointDecl(@NonNull ImmutableList mods, - JmlParser.@NonNull Merge_point_statementContext mergeProc) { + private final JmlParser.Merge_point_statementContext mergeProc; + + public TextualJMLMergePointDecl(ImmutableList mods, + JmlParser.Merge_point_statementContext mergeProc) { super(mods); this.mergeProc = mergeProc; setPosition(mergeProc); } - public JmlParser.@NonNull Merge_point_statementContext getMergeProc() { + public JmlParser.Merge_point_statementContext getMergeProc() { return mergeProc; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/Context.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/Context.java index 4e1aa8ca937..e065b75d7aa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/Context.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/Context.java @@ -66,7 +66,7 @@ public static Context inMethodWithSelfVar(@NonNull IProgramMethod pm, ProgramVar * @param tb term builder */ public static Context inClass(@NonNull KeYJavaType classType, boolean isStaticContext, - TermBuilder tb) { + TermBuilder tb) { var selfVar = createSelfVar(tb, classType, isStaticContext); var mode = JMLInfoExtractor.getSpecMathModeOrDefault(classType); return new Context(mode, classType, selfVar); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index f80ff858970..bd0a85fc4a8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -1169,8 +1169,9 @@ public Contract createJMLDependencyContract(KeYJavaType kjt, TextualJMLDepends t LabeledParserRuleContext dep = null; LocationVariable targetHeap = null; for (LocationVariable heap : HeapContext.getModHeaps(services, false)) { - dep = textualDep.getDepends(heap.name()).head(); - if (dep != null) { + ImmutableList depends = textualDep.getDepends(heap.name()); + if (!depends.isEmpty()) { + dep = textualDep.getDepends(heap.name()).head(); targetHeap = heap; break; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java index cc92631fe6f..bacbae1a9e1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java @@ -12,7 +12,6 @@ import org.jspecify.annotations.Nullable; - public class SLTranslationException extends ProofInputException implements HasLocation { protected final Location location; diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/KeYTypeUtil.java b/key.core/src/main/java/de/uka/ilkd/key/util/KeYTypeUtil.java index 59d63f49128..e87e74b8cce 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/KeYTypeUtil.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/KeYTypeUtil.java @@ -18,6 +18,8 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.java.CollectionUtil; +import org.jspecify.annotations.Nullable; + /** * Provides utility methods which makes it easier to analyze the type hierarchy of * {@link KeYJavaType} instances with help of given {@link Services}. @@ -59,7 +61,7 @@ public static boolean isInnerType(Services services, KeYJavaType type) { * @param type The type. * @return The parent package/type or {@code null} if it has no one. */ - public static String getParentName(Services services, KeYJavaType type) { + public static @Nullable String getParentName(Services services, @Nullable KeYJavaType type) { return type != null ? getParentName(services, type.getFullName()) : null; } @@ -70,7 +72,7 @@ public static String getParentName(Services services, KeYJavaType type) { * @param fullName The name of the current package/type. * @return The parent package/type or {@code null} if it has no one. */ - private static String getParentName(Services services, String fullName) { + private static @Nullable String getParentName(Services services, String fullName) { int lastSeparator = fullName.lastIndexOf(PACKAGE_SEPARATOR); if (lastSeparator >= 0) { String parentName = fullName.substring(0, lastSeparator); @@ -106,7 +108,7 @@ public static boolean isType(Services services, String fullName) { * @param fullName The full name of the requested {@link KeYJavaType}. * @return The found {@link KeYJavaType} or {@code null} if no type exist with the given name. */ - public static KeYJavaType getType(Services services, String fullName) { + public static @Nullable KeYJavaType getType(Services services, String fullName) { try { return services.getJavaInfo().getKeYJavaType(fullName); } catch (Exception e) { @@ -145,7 +147,7 @@ public static boolean isImplicitConstructor(IProgramMethod pm) { * @param implicitConstructor The implicit constructor. * @return The found explicit constructor or {@code null} if not available. */ - public static IProgramMethod findExplicitConstructor(Services services, + public static @Nullable IProgramMethod findExplicitConstructor(Services services, final IProgramMethod implicitConstructor) { if (services != null && implicitConstructor != null) { ImmutableList pms = diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java index 0ce8a09b6c4..71b3da65b64 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/package-info.java @@ -3,4 +3,7 @@ * side functionalities like the installer (subpackage install), and the tool for * removing generics from a Java program (subpackage removegenerics). */ +@NullMarked package de.uka.ilkd.key.util; + +import org.jspecify.annotations.NullMarked; diff --git a/key.ncore/src/main/java/module-info.java b/key.ncore/src/main/java/module-info.java deleted file mode 100644 index 409c7c0a9b9..00000000000 --- a/key.ncore/src/main/java/module-info.java +++ /dev/null @@ -1,9 +0,0 @@ -module org.key_project.ncore { - requires org.key_project.util; - requires org.jspecify; - - /* requires, exports, uses */ - exports org.key_project.logic; - exports org.key_project.logic.op; - exports org.key_project.logic.sort; -} \ No newline at end of file diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java index 6e36b867321..1cdfd42159d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java @@ -675,7 +675,11 @@ private void updatePreview(PositionedIssueString issue) { String source = StringUtil.replaceNewlines( fileContentsCache.computeIfAbsent(uri, fn -> { try { - return IOUtil.readFrom(finalUri).orElseThrow(); + String result = IOUtil.readFrom(finalUri); + if (result == null) { + throw new NullPointerException(); + } + return result; } catch (IOException e) { LOGGER.debug("Unknown IOException!", e); return "[SOURCE COULD NOT BE LOADED]\n" + e.getMessage(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java index 52e58dcbec8..ad670bf962a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java @@ -138,10 +138,10 @@ public void addNotify() { } }; Optional file = location.getFileURI(); - String source = IOUtil.readFrom(file.orElse(null)).orElse(""); + String source = IOUtil.readFrom(file.orElse(null)); // workaround for #1641: replace all carriage returns, since JavaDocument can currently // not handle them - source = source.replace("\r", ""); + source = source != null ? source.replace("\r", "") : ""; if (file.isPresent() && file.get().toString().endsWith(".java")) { JavaDocument doc = new JavaDocument(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java index 1d87d1712ac..59a6e71cee5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java @@ -13,7 +13,6 @@ import java.nio.file.Files; import java.util.LinkedList; import java.util.List; -import java.util.Optional; import java.util.zip.ZipEntry; import java.util.zip.ZipOutputStream; import javax.swing.*; @@ -287,9 +286,8 @@ byte[] retrieveFileData() throws IOException { URI url = ExceptionTools.getLocation(throwable) .flatMap(Location::getFileURI) .orElse(null); - Optional content = IOUtil.readFrom(url); - return content.map(s -> s.getBytes(Charset.defaultCharset())) - .orElse(new byte[0]); + String content = IOUtil.readFrom(url); + return content != null ? content.getBytes(Charset.defaultCharset()) : new byte[0]; } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java index 86d45f5a195..622b4adeb1c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java @@ -22,8 +22,6 @@ import org.jspecify.annotations.NonNull; - - /* * Search bar implementing search function for SequentView. */ diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java index 2f937cdc2fa..55d8af0c3d9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIAbstractTreeNode.java @@ -13,7 +13,6 @@ import org.jspecify.annotations.NonNull; - public abstract class GUIAbstractTreeNode implements TreeNode { private final GUIProofTreeModel tree; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeExpansionState.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeExpansionState.java index 48c8aa81a54..8402266b162 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeExpansionState.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeExpansionState.java @@ -18,7 +18,6 @@ import org.jspecify.annotations.NonNull; - /** * Cache/Access JTree's expansion state. The interface of JTree to access the expanded paths is * rather incomplete, since expanded paths under collapsed ancestors cannot be accessed at all diff --git a/key.util/Readme.md b/key.util/Readme.md new file mode 100644 index 00000000000..0da4579914a --- /dev/null +++ b/key.util/Readme.md @@ -0,0 +1,104 @@ +# key.util + +This subproject contains various data structures and utility functions +used by the KeY project. + +## Nullness checking + +This subproject uses the EISOP branch of the Checker Framework +(https://eisop.github.io/) to check for nullness-related +errors at compile time. + +Any use of a type is considered to be `@NonNull` by default unless `@Nullable` +is specified. E.g., a variable of type `@Nullable Object` cannot be assigned +to a variable of type `@NonNull Object`. + +This is for the most part intuitive, but arrays and generics require some +explanation: +For an array, we specify the nullability of both the array and elements. +E.g., `@Nullable String @NonNull []` is a non-null array of nullable strings. +The nullability of a generic type is determined by its bounds. E.g., if we +have a class `class A`, then any use of `T` in `A` +is implicitly nullable; but if we have a class `class B`, then any use of +`S` in `B` is implicitly non-null because this is the default bound. + +For further details, see +https://jspecify.dev/docs/api/org/jspecify/annotations/package-summary.html +and +https://eisop.github.io/cf/manual/manual.html#nullness-checker + +## Initialization checking + +The Checker Framework also checks for initialization: If a constructor does +not initialize every `@NonNull` field with a non-null value, an error to that +effect is reported at compile time. If a constructor tries to call a non-helper +method, an error is also reported, as that method may rely on all `@NonNull` +fields being initialized. +You can mark a method as helper by specifying +`@UnderInitialization(InitClass.class) ReceiverClass this` as the first +parameter, where `ReceiverClass` is the name of the current class, and +`InitClass` is the class up to which `this` should be initialized before +the method is allowed to be called. +If you want to allow the helper method being called even after `this` has been +further initialized, use `@UnknownInitialization(InitClass.class)` instead. +Within a helper method, all possibly uninitialized fields are considered +`@Nullable` even if declared as `@NonNull`. + +E.g., consider the following listing. + +```java +class A { + @NonNull Object fieldA; + + A() { + fieldA = new Object(); + } +} + +class B extends A { + @NonNull Object fieldB; + + B() { + super(); + // Allowed because the super constructor has initialized this up to A + helperA(); + + // Not allowed because this is not yet initialized up to B + helperB(); + + fieldB = new Object(); + + // Allowed now because fieldB was just initialized + helperB(); + + // Not allowed because B is not final; thus there may be a subclass + // for which this has not yet been initialized. + nonHelper(); + } + + void helperA(@UnderInitialization(A.class) B this) { + // Allowed because this is initialized up to A; + // thus fieldA is @NonNull + fieldA.hashCode(); + // Not allowed because this is not initialized up to B; + // thus fieldB is @Nullable + fieldB.hashCode(); + } + + void helperB(@UnderInitialization(B.class) B this) { + // Both allowed because this is initialized up to B + fieldA.hashCode(); + fieldB.hashCode(); + } + + void nonHelper() { + // ... + } +} +``` + +The initialization types for arrays and generics are specified in the same way +as for nullness types. + +For more details, see +https://eisop.github.io/cf/manual/manual.html#initialization-checker \ No newline at end of file diff --git a/key.util/build.gradle b/key.util/build.gradle index 48d89172e19..25700d3ec91 100644 --- a/key.util/build.gradle +++ b/key.util/build.gradle @@ -2,4 +2,20 @@ description "Utility library of the key-project" dependencies { implementation("org.jspecify:jspecify:0.3.0") -} \ No newline at end of file +} + +checkerFramework { + if(System.getProperty("ENABLE_NULLNESS")) { + checkers = [ + "org.checkerframework.checker.nullness.NullnessChecker", + ] + extraJavacArgs = [ + "-AonlyDefs=^org\\.key_project\\.util", + "-Xmaxerrs", "10000", + "-Astubs=$projectDir/src/main/checkerframework:permit-nullness-assertion-exception.astub", + "-AstubNoWarnIfNotFound", + "-Werror", + "-Aversion", + ] + } +} diff --git a/key.util/src/main/checkerframework/java/net/URI.astub b/key.util/src/main/checkerframework/java/net/URI.astub new file mode 100644 index 00000000000..c4f24eb79e0 --- /dev/null +++ b/key.util/src/main/checkerframework/java/net/URI.astub @@ -0,0 +1,14 @@ +package java.net; + +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.framework.qual.AnnotatedFor; + +@AnnotatedFor("nullness") +public class URI { + + public URI(@Nullable String scheme, + @Nullable String userInfo, @Nullable String host, int port, + @Nullable String path, @Nullable String query, @Nullable String fragment) + throws URISyntaxException {} + +} diff --git a/key.util/src/main/java/module-info.java b/key.util/src/main/java/module-info.java deleted file mode 100644 index f48836b67ef..00000000000 --- a/key.util/src/main/java/module-info.java +++ /dev/null @@ -1,15 +0,0 @@ -module org.key_project.util { - requires java.desktop; - requires org.jspecify; - - exports org.key_project.util.bean; - exports org.key_project.util.collection; - exports org.key_project.util.bitops; - exports org.key_project.util.helper; - exports org.key_project.util.java; - exports org.key_project.util.java.thread; - exports org.key_project.util.lookup; - exports org.key_project.util.reflection; - exports org.key_project.util.testcategories; - exports org.key_project.util; -} \ No newline at end of file diff --git a/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyUtil.java b/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyUtil.java index f1caf2637ca..599ed7d6741 100644 --- a/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyUtil.java +++ b/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyUtil.java @@ -13,6 +13,7 @@ * * @author Arne Keller */ +@SuppressWarnings("nullness") public final class EqualsModProofIrrelevancyUtil { private EqualsModProofIrrelevancyUtil() { diff --git a/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyWrapper.java b/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyWrapper.java index d9ace447c10..b0b78f7f5ee 100644 --- a/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyWrapper.java +++ b/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyWrapper.java @@ -12,6 +12,7 @@ * @param type to wrap * @author Arne Keller */ +@SuppressWarnings("nullness") public class EqualsModProofIrrelevancyWrapper { /** * The wrapped object. diff --git a/key.util/src/main/java/org/key_project/util/ExtList.java b/key.util/src/main/java/org/key_project/util/ExtList.java index 3ac1566e0d9..b13b4f23cb2 100644 --- a/key.util/src/main/java/org/key_project/util/ExtList.java +++ b/key.util/src/main/java/org/key_project/util/ExtList.java @@ -8,12 +8,13 @@ import java.util.Iterator; import java.util.LinkedList; +import org.jspecify.annotations.Nullable; /** * Extends java.util.LinkedList in order to collect elements according to their type. * Has facilities to get elements of a certain type ({@link #get(Class)}, {@link #collect(Class)}). */ -public class ExtList extends LinkedList { +public final class ExtList extends LinkedList { private static final long serialVersionUID = 9182017368310263908L; @@ -60,7 +61,7 @@ public T[] collect(Class cl) { * @return the first element with type cl in list */ @SuppressWarnings("unchecked") - public T get(Class cl) { + public @Nullable T get(Class cl) { for (Object next : this) { if (cl.isInstance(next) && (next != null)) { return (T) next; @@ -78,7 +79,7 @@ public T get(Class cl) { * @return the first element with type cl in list */ @SuppressWarnings("unchecked") - public T removeFirstOccurrence(Class cl) { + public @Nullable T removeFirstOccurrence(Class cl) { Iterator it = iterator(); while (it.hasNext()) { Object next = it.next(); diff --git a/key.util/src/main/java/org/key_project/util/Filenames.java b/key.util/src/main/java/org/key_project/util/Filenames.java index f2160054131..9f0c7eb4e7d 100644 --- a/key.util/src/main/java/org/key_project/util/Filenames.java +++ b/key.util/src/main/java/org/key_project/util/Filenames.java @@ -156,7 +156,9 @@ private static String[] removeDotDot(String[] a) { if (!a[a.length - 1].equals("..")) { newa[k++] = a[a.length - 1]; } - return Arrays.copyOf(newa, k); + // @ assert (\forall int i; 0 <= i < k; newa[i] != null); + // TODO: nullness. This cast cannot be checked, can it? But there is no error message + return (String[]) Arrays.copyOf(newa, k); } public static String toValidFileName(String s) { diff --git a/key.util/src/main/java/org/key_project/util/RandomName.java b/key.util/src/main/java/org/key_project/util/RandomName.java index 2b21c81c758..ff58440b2b1 100644 --- a/key.util/src/main/java/org/key_project/util/RandomName.java +++ b/key.util/src/main/java/org/key_project/util/RandomName.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util; + import java.util.Random; /** diff --git a/key.util/src/main/java/org/key_project/util/Streams.java b/key.util/src/main/java/org/key_project/util/Streams.java index 7840a975ead..d1eecb6a03d 100644 --- a/key.util/src/main/java/org/key_project/util/Streams.java +++ b/key.util/src/main/java/org/key_project/util/Streams.java @@ -8,7 +8,6 @@ import java.io.InputStream; public class Streams { - private Streams() { throw new Error("do not instantiate"); } diff --git a/key.util/src/main/java/org/key_project/util/Strings.java b/key.util/src/main/java/org/key_project/util/Strings.java index 200cc051283..f30a81a28ac 100644 --- a/key.util/src/main/java/org/key_project/util/Strings.java +++ b/key.util/src/main/java/org/key_project/util/Strings.java @@ -3,13 +3,15 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util; - +import java.util.Objects; import java.util.function.Function; -import java.util.regex.Matcher; -import java.util.regex.Pattern; import java.util.stream.Collectors; import java.util.stream.StreamSupport; +import org.key_project.util.java.StringUtil; + +import org.jspecify.annotations.Nullable; + /** * Helper functions for {@link String}s * @@ -18,44 +20,22 @@ */ public class Strings { /** - * Checks whether a string contains another one as a whole word (i.e., separated by whitespaces - * or a semicolon at the end). - * - * @param s string to search in - * @param word string to be searched for + * @deprecated This class has been merged with {@link org.key_project.util.java.StringUtil}. + * Call + * {@link org.key_project.util.java.StringUtil#containsWholeWord(String, String)} */ + @Deprecated public static boolean containsWholeWord(String s, String word) { - Pattern p = Pattern.compile("\\b" + word + "\\b"); - Matcher m = p.matcher(s); - return m.find(); - /* - * if (s == null || word == null) { return false; } int i = -1; final int wl = - * word.length(); while (true) { i = s.indexOf(word, i + 1); if (i < 0 || i >= s.length()) - * break; if (i == 0 || Character.isWhitespace(s.charAt(i - 1))) { if (i + wl == s.length() - * || Character.isWhitespace(s.charAt(i + wl)) || s.charAt(i + wl) == ';') { return true; } - * } } return false; - */ + return StringUtil.containsWholeWord(s, word); } - /** - * There are different kinds of JML markers. See Section 4.4 "Annotation markers" of the JML - * reference manual. - * - * @param comment - * @return + * @deprecated This class has been merged with {@link org.key_project.util.java.StringUtil}. + * Call {@link org.key_project.util.java.StringUtil#isJMLComment(String)} */ + @Deprecated public static boolean isJMLComment(String comment) { - try { - return (comment.startsWith("/*@") || comment.startsWith("//@") - || comment.startsWith("/*+KeY@") || comment.startsWith("//+KeY@") - || (comment.startsWith("/*-") && !comment.startsWith("KeY", 3) - && comment.contains("@")) - || (comment.startsWith("//-") && !comment.startsWith("KeY", 3) - && comment.contains("@"))); - } catch (IndexOutOfBoundsException e) { - return false; - } + return StringUtil.isJMLComment(comment); } /** @@ -70,11 +50,12 @@ public static boolean isJMLComment(String comment) { * @return the CharSequence in the described format * @param the type of the elements of the iterated collection */ - public static String formatAsList(Iterable it, + public static String formatAsList( + Iterable it, CharSequence open, CharSequence sep, CharSequence close, Function mapper) { return StreamSupport.stream(it.spliterator(), false) - .map(a -> mapper.apply(a).toString()) + .map(a -> Objects.toString(mapper.apply(a))) .collect(Collectors.joining(sep, open, close)); } @@ -89,7 +70,7 @@ public static String formatAsList(Iterable it, * @return the CharSequence in the described format * @param the type of the elements of the iterated collection */ - public static String formatAsList(Iterable it, + public static String formatAsList(Iterable it, CharSequence open, CharSequence sep, CharSequence close) { return formatAsList(it, open, sep, close, Function.identity()); } diff --git a/key.util/src/main/java/org/key_project/util/bean/Bean.java b/key.util/src/main/java/org/key_project/util/bean/Bean.java index de4ac6f2f7a..7c3a46c0391 100644 --- a/key.util/src/main/java/org/key_project/util/bean/Bean.java +++ b/key.util/src/main/java/org/key_project/util/bean/Bean.java @@ -9,6 +9,8 @@ import org.key_project.util.java.ArrayUtil; +import org.jspecify.annotations.Nullable; + /** * Implements the basic methods that a Java bean should have and is the default implementation of * {@link IBean}. @@ -20,6 +22,7 @@ public class Bean implements IBean { /** * The used {@link PropertyChangeSupport}. */ + @SuppressWarnings("nullness") // TODO Check with Werner Dietl why this is so. private final PropertyChangeSupport pcs = new PropertyChangeSupport(this); /** @@ -129,8 +132,8 @@ protected void fireIndexedPropertyChange(String propertyName, int index, int old * @param oldValue The old value. * @param newValue The new value. */ - protected void fireIndexedPropertyChange(String propertyName, int index, Object oldValue, - Object newValue) { + protected void fireIndexedPropertyChange(String propertyName, int index, + @Nullable Object oldValue, @Nullable Object newValue) { pcs.fireIndexedPropertyChange(propertyName, index, oldValue, newValue); } diff --git a/key.util/src/main/java/org/key_project/util/bean/package-info.java b/key.util/src/main/java/org/key_project/util/bean/package-info.java new file mode 100644 index 00000000000..0cf610b9f7b --- /dev/null +++ b/key.util/src/main/java/org/key_project/util/bean/package-info.java @@ -0,0 +1,4 @@ +@NullMarked +package org.key_project.util.bean; + +import org.jspecify.annotations.NullMarked; diff --git a/key.util/src/main/java/org/key_project/util/bitops/ImmutableFixedLengthBitSet.java b/key.util/src/main/java/org/key_project/util/bitops/ImmutableFixedLengthBitSet.java index 56f92c9595c..e501d56e68c 100644 --- a/key.util/src/main/java/org/key_project/util/bitops/ImmutableFixedLengthBitSet.java +++ b/key.util/src/main/java/org/key_project/util/bitops/ImmutableFixedLengthBitSet.java @@ -6,16 +6,19 @@ import java.util.ArrayList; import java.util.BitSet; +import org.jspecify.annotations.NullMarked; + /** * Represents a non-negative number with access to single bits; the length of the bit set is fixed. * Comparable to {@link BitSet} with fixed length. Objects of this class are immutable. * * @author Dominic Scheurer */ +@NullMarked public class ImmutableFixedLengthBitSet { - private boolean[] bitSet = null; - private int value = -1; + private final boolean[] bitSet; + private int value; /** * Constructs a new {@link ImmutableFixedLengthBitSet} for the given length. All bits are set to diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java b/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java index aeecc7916dc..bc976b8c70c 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java @@ -9,6 +9,7 @@ * * @author Arne Keller */ +@SuppressWarnings("nullness") public class DefaultEdge implements GraphEdge { /** * Source node of this edge. diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java index 2181760ca64..2b5b6cd5056 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java @@ -11,6 +11,7 @@ * This class implements {@code ImmutableMap} and provides a persistent map. * It is a simple implementation like lists */ +@SuppressWarnings("nullness") public class DefaultImmutableMap implements ImmutableMap { /** diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java index d35264c12f3..ba1af27f3c9 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java @@ -3,10 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.collection; -import java.util.Collection; -import java.util.HashSet; -import java.util.Iterator; -import java.util.Set; +import java.util.*; import java.util.function.Predicate; import java.util.stream.Stream; import java.util.stream.StreamSupport; @@ -21,7 +18,7 @@ * * @param type of object to store */ -public class DefaultImmutableSet implements ImmutableSet { +public class DefaultImmutableSet implements ImmutableSet { /** * @@ -38,7 +35,7 @@ public class DefaultImmutableSet implements ImmutableSet { /** the empty set */ @SuppressWarnings("unchecked") - public static DefaultImmutableSet nil() { + public static DefaultImmutableSet nil() { return (DefaultImmutableSet) NILSet.NIL; } @@ -51,7 +48,7 @@ protected DefaultImmutableSet() { * * @param element of type the new Set contains */ - protected DefaultImmutableSet(T element) { + private DefaultImmutableSet(T element) { elementList = (ImmutableSLList.nil()).prepend(element); } @@ -65,6 +62,10 @@ private DefaultImmutableSet(ImmutableList elementList) { this.elementList = elementList; } + public static ImmutableSet fromCollection(Collection seq) { + return new DefaultImmutableSet<>(ImmutableList.fromList(seq)); + } + // private static HashSet previousComplains = new HashSet<>(); private void complainAboutSize() { // // Immutable linear sets are very expensive with O(n) addition @@ -234,7 +235,7 @@ public ImmutableSet remove(T element) { * @return true iff the this set is subset of o and vice versa. */ @Override - public boolean equals(Object obj) { + public boolean equals(@Nullable Object obj) { if (obj == this) { return true; } @@ -289,7 +290,8 @@ public ImmutableList toImmutableList() { * @param list a non-null immutable list * @return a fresh immutable set with the same iteration order. */ - public static ImmutableSet fromImmutableList(ImmutableList list) { + public static ImmutableSet fromImmutableList( + ImmutableList list) { if (list.isEmpty()) { return nil(); } else { @@ -297,36 +299,6 @@ public static ImmutableSet fromImmutableList(ImmutableList list) { } } - /** - * Create an immutable set from a mutable set - * - * @param set a non-null mutable set - * @return a fresh immutable set with all the elements in set - */ - public static ImmutableSet fromSet(@Nullable Set set) { - if (set == null) { - return null; - } - if (set.isEmpty()) { - return nil(); - } else { - ImmutableList backerList = ImmutableSLList.nil(); - for (T element : set) { - backerList = backerList.prepend(element); - } - return new DefaultImmutableSet<>(backerList); - } - } - - - public static ImmutableSet fromCollection(@Nullable Collection seq) { - if (seq == null) { - return null; - } - return fromSet(new HashSet<>(seq)); - } - - @Override public String toString() { return Strings.formatAsList(this, "{", ",", "}"); @@ -403,10 +375,10 @@ public boolean isEmpty() { } /** - * @return true iff the this set is subset of o and vice versa. + * @return true iff this set is subset of o and vice versa. */ @Override - public boolean equals(Object o) { + public boolean equals(@Nullable Object o) { return o instanceof NILSet; } diff --git a/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java b/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java index 3f48bef5442..921359281ad 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java +++ b/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java @@ -17,6 +17,7 @@ * @param edge type * @author Arne Keller */ +@SuppressWarnings("nullness") public class DirectedGraph implements Graph { /** * Set of vertices in this graph. diff --git a/key.util/src/main/java/org/key_project/util/collection/IdentityHashSet.java b/key.util/src/main/java/org/key_project/util/collection/IdentityHashSet.java index 0c4d1408f30..f68a9b8a6b9 100644 --- a/key.util/src/main/java/org/key_project/util/collection/IdentityHashSet.java +++ b/key.util/src/main/java/org/key_project/util/collection/IdentityHashSet.java @@ -8,17 +8,19 @@ import java.util.Iterator; import java.util.Set; +import org.jspecify.annotations.Nullable; + /** * Hash set using the object's identity instead of their hashcode to determine uniqueness. * * @param elmeent type * @author Arne Keller */ -public class IdentityHashSet implements Set { +public final class IdentityHashSet implements Set { /** * Backing store. */ - private final IdentityHashMap innerMap = new IdentityHashMap<>(); + private final IdentityHashMap innerMap = new IdentityHashMap<>(); /** * Construct an empty set. @@ -47,7 +49,7 @@ public boolean isEmpty() { } @Override - public boolean contains(Object o) { + public boolean contains(@Nullable Object o) { return innerMap.containsKey(o); } @@ -56,13 +58,17 @@ public Iterator iterator() { return innerMap.keySet().iterator(); } + // see https://eisop.github.io/cf/manual/manual.html#nullness-collection-toarray + @SuppressWarnings({ "nullness", "override.return.invalid" }) @Override - public Object[] toArray() { + public @Nullable Object[] toArray() { return innerMap.keySet().toArray(); } + // see https://eisop.github.io/cf/manual/manual.html#nullness-collection-toarray + @SuppressWarnings({ "nullness", "override.return.invalid" }) @Override - public T1[] toArray(T1[] a) { + public T[] toArray(T[] a) { return innerMap.keySet().toArray(a); } @@ -72,7 +78,7 @@ public boolean add(T o) { } @Override - public boolean remove(Object o) { + public boolean remove(@Nullable Object o) { var contained = innerMap.containsKey(o); innerMap.remove(o); return contained; @@ -101,6 +107,8 @@ public boolean removeAll(Collection c) { return changed; } + + @Override public boolean retainAll(Collection c) { return innerMap.keySet().retainAll(c); diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java index aefc3822e32..e102f797603 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java @@ -16,6 +16,7 @@ import org.jspecify.annotations.NonNull; +@SuppressWarnings("nullness") public class ImmutableArray implements java.lang.Iterable, java.io.Serializable { /** diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableLeftistHeap.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableLeftistHeap.java index 9b981683b32..b0dee24b25b 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableLeftistHeap.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableLeftistHeap.java @@ -12,6 +12,7 @@ * This class implements the leftist heap, see "Functional Data Structures" by Chris * Okasaki */ +@SuppressWarnings("nullness") public abstract class ImmutableLeftistHeap> implements ImmutableHeap { /** diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java index 6fd1ec96f77..b46809d980a 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java @@ -10,19 +10,21 @@ import java.util.stream.Stream; import java.util.stream.StreamSupport; -import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** * List interface to be implemented by non-destructive lists */ -public interface ImmutableList extends Iterable, java.io.Serializable { +public interface ImmutableList + extends Iterable, java.io.Serializable { /** * Returns a Collector that accumulates the input elements into a new ImmutableList. * * @return a Collector that accumulates the input elements into a new ImmutableList. */ - static Collector, ImmutableList> collector() { + @SuppressWarnings("nullness") // it seems some annotations are missing on Collector.of ... + static Collector, ImmutableList> collector() { return Collector.of(LinkedList::new, List::add, (list1, list2) -> { list1.addAll(list2); return list1; @@ -35,7 +37,7 @@ static Collector, ImmutableList> collector() { * @param list a List. * @return an ImmutableList containing the same elements as the specified list. */ - static ImmutableList fromList(Collection list) { + static ImmutableList fromList(Collection list) { ImmutableList result = ImmutableSLList.nil(); for (T el : list) { @@ -51,7 +53,7 @@ static ImmutableList fromList(Collection list) { * @return empty immutable list. * @param the entry type of the list. */ - static ImmutableList of() { + static ImmutableList of() { return ImmutableSLList.nil(); } @@ -62,7 +64,7 @@ static ImmutableList of() { * @return singleton immutable list. * @param the entry type of the list. */ - static ImmutableList of(T e1) { + static ImmutableList of(T e1) { return ImmutableSLList.singleton(e1); } @@ -75,7 +77,7 @@ static ImmutableList of(T e1) { * @return (e1, e2) as immutable list * @param the entry type of the list. */ - static ImmutableList of(T e1, T e2) { + static ImmutableList of(T e1, T e2) { return ImmutableSLList.singleton(e2).prepend(e1); } @@ -89,7 +91,7 @@ static ImmutableList of(T e1, T e2) { * @return (e1, e2, e3) as immutable list * @param the entry type of the list. */ - static ImmutableList of(T e1, T e2, T e3) { + static ImmutableList of(T e1, T e2, T e3) { return ImmutableSLList.singleton(e3).prepend(e2).prepend(e1); } @@ -101,7 +103,7 @@ static ImmutableList of(T e1, T e2, T e3) { * @return (e1, e2, e3, ...) as immutable list * @param the entry type of the list. */ - static ImmutableList of(T... es) { + static ImmutableList of(T... es) { ImmutableList result = ImmutableSLList.nil(); for (int i = es.length - 1; i >= 0; i--) { result = result.prepend(es[i]); @@ -190,7 +192,7 @@ static ImmutableList of(T... es) { * @param predicate the predicate * @return true if predicate is fullfilled for at least one element */ - boolean exists(Predicate predicate); + boolean exists(Predicate predicate); /** * @return IList tail of list @@ -228,6 +230,7 @@ static ImmutableList of(T... es) { /** * @return true iff the list is empty */ + // not true: @EnsuresNonNullIf(expression = {"head()"}, result = false) boolean isEmpty(); /** @@ -247,12 +250,12 @@ static ImmutableList of(T... es) { /** * Convert the list to a Java array (O(n)) */ - S[] toArray(S[] array); + S[] toArray(S[] array); /** * Convert the list to a Java array (O(n)) */ - S[] toArray(Class type); + S[] toArray(Class type); /** @@ -287,7 +290,7 @@ default List toList() { * * @returns the filtered list */ - default @NonNull ImmutableList filter(@NonNull Predicate predicate) { + default ImmutableList filter(Predicate predicate) { return Immutables.filter(this, predicate); } @@ -299,7 +302,7 @@ default List toList() { * @param function a non-interfering, stateless function to apply to each element * @return the mapped list of the same length as this */ - default ImmutableList map(Function function) { + default ImmutableList map(Function function) { return Immutables.map(this, function); } @@ -307,7 +310,7 @@ default ImmutableList map(Function function) { * @param other prefix to check for * @return whether this list starts with the elements of the provided prefix */ - default boolean hasPrefix(ImmutableList other) { + default boolean hasPrefix(ImmutableList other) { if (other.size() > this.size()) { return false; } @@ -328,7 +331,7 @@ default boolean hasPrefix(ImmutableList other) { * @return new list with the prefix removed * @throws IllegalArgumentException if the provided prefix is not a prefix of this list */ - default ImmutableList stripPrefix(ImmutableList prefix) { + default ImmutableList stripPrefix(ImmutableList prefix) { if (prefix.isEmpty()) { return this; } @@ -352,7 +355,9 @@ default T last() { while (!remainder.tail().isEmpty()) { remainder = remainder.tail(); } - return remainder.head(); + T result = remainder.head(); + assert result != null : "@AssumeAssertion(nullness): this should never be null"; + return result; } /** diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java index 50106229327..7e52f453ee0 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java @@ -14,6 +14,11 @@ import org.key_project.util.Strings; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * Simple implementation of a non-destructive (unmodifiable) list. The list implementation allows * list sharing of sublists. @@ -24,22 +29,21 @@ * appending and prepending and element can be realized with O(1) costs (see Osaka) then having tail * and head with amortized O(1). This will be done later (if necessary). */ - -@SuppressWarnings("unchecked") -public abstract class ImmutableSLList implements ImmutableList { +@SuppressWarnings({ "unchecked" }) +public abstract class ImmutableSLList implements ImmutableList { /** * generated serial id */ private static final long serialVersionUID = 8717813038177120287L; - + private static final Logger log = LoggerFactory.getLogger(ImmutableSLList.NIL.class); /** the empty list */ - public static ImmutableSLList nil() { + public static ImmutableSLList nil() { return (ImmutableSLList) NIL.NIL; } - public static ImmutableSLList singleton(T obj) { + public static ImmutableSLList singleton(T obj) { return new Cons<>(obj, nil()); } @@ -65,10 +69,13 @@ public ImmutableList reverse() { * Convert the list to a Java array (O(n)) */ @Override - public S[] toArray(S[] array) { + public S[] toArray(S[] array) { S[] result; if (array.length < size()) { - result = (S[]) Array.newInstance(array.getClass().getComponentType(), size()); + Class arrayClass = array.getClass(); + assert arrayClass.isArray() + : "@AssumeAssertion(nullness): This has indeed a component type"; + result = (S[]) Array.newInstance(arrayClass.getComponentType(), size()); } else { result = array; } @@ -84,11 +91,14 @@ public S[] toArray(S[] array) { * Convert the list to a Java array (O(n)) */ @Override - public S[] toArray(Class type) { + @SuppressWarnings("nullness") + public S[] toArray(Class type) { S[] result = (S[]) Array.newInstance(type, size()); ImmutableList rest = this; for (int i = 0, sz = size(); i < sz; i++) { - result[i] = (S) rest.head(); + // @ assert !rest.isEmpty(); + T head = rest.head(); + result[i] = (S) type.cast(head); rest = rest.tail(); } return result; @@ -165,7 +175,7 @@ public ImmutableList take(int n) { } - private static class Cons extends ImmutableSLList { + private static class Cons extends ImmutableSLList { /** * @@ -226,7 +236,11 @@ public ImmutableList prepend(ImmutableList list) { } else { final int sz = list.size(); if (sz == 1) { - return new Cons<>(list.head(), this); + // @ assert !list.isEmpty(); + @SuppressWarnings("nullness") + @NonNull + S head = list.head(); + return new Cons<>(head, this); } Cons result = this; final Object[] listElements = list.toArray(new Object[sz]); @@ -250,6 +264,7 @@ public ImmutableList prependReverse(ImmutableList list) { } else { Cons result = this; for (int sz = list.size(); sz > 0; sz--) { + assert !list.isEmpty() : "@AssumeAssertion(nullness): Invariant"; result = new Cons<>(list.head(), result); list = list.tail(); } @@ -264,7 +279,7 @@ public ImmutableList prependReverse(ImmutableList list) { * @return true if predicate is fullfilled for at least one element */ @Override - public boolean exists(Predicate predicate) { + public boolean exists(Predicate predicate) { ImmutableList list = this; while (!list.isEmpty()) { if (predicate.test(list.head())) { @@ -284,7 +299,7 @@ public boolean exists(Predicate predicate) { */ @Override public ImmutableList append(S e) { - return new Cons<>(e).prepend(this); + return new Cons(e).prepend(this); } /** @@ -429,7 +444,7 @@ public ImmutableList removeAll(S obj) { @Override - public boolean equals(Object o) { + public boolean equals(@Nullable Object o) { if (!(o instanceof ImmutableList)) { return false; } @@ -458,7 +473,7 @@ public String toString() { } /** iterates through a none destructive list */ - private static class SLListIterator implements Iterator { + private static class SLListIterator implements Iterator { /** the list of remaining elements */ private ImmutableList list; @@ -475,6 +490,7 @@ public SLListIterator(ImmutableList list) { /** @return next element in list */ @Override public T next() { + // TODO Perhaps add a RT and throw NuSuchElement to make type checker happy. final T element = list.head(); list = list.tail(); return element; @@ -529,7 +545,7 @@ public int size() { } @Override - public boolean equals(Object o) { + public boolean equals(@Nullable Object o) { return o instanceof NIL; } @@ -580,7 +596,7 @@ public boolean contains(S obj) { * @return true if predicate is fullfilled for at least one element */ @Override - public boolean exists(Predicate predicate) { + public boolean exists(Predicate predicate) { return false; } @@ -596,7 +612,9 @@ public Iterator iterator() { @Override public S head() { - return null; + NoSuchElementException ex = new NoSuchElementException(); + log.error("head on NIL!", ex); + throw ex; } @Override @@ -631,7 +649,7 @@ public SLNilListIterator() { /** @return next element in list */ @Override public S next() { - return null; + throw new NoSuchElementException(); } /** diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java index 9b1dcf7381c..ec69790c40d 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java @@ -9,60 +9,40 @@ import java.util.stream.Collector.Characteristics; import java.util.stream.Stream; -import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** * interface implemented by non-destructive Sets. CONVENTION: Each SetOf implementation has to * offer a public static final variable .nil() */ - -public interface ImmutableSet extends Iterable, java.io.Serializable { +public interface ImmutableSet + extends Iterable, java.io.Serializable { /** * Returns a Collector that accumulates the input elements into a new ImmutableSet. * * @return a Collector that accumulates the input elements into a new ImmutableSet. */ - static Collector, ImmutableSet> collector() { + @SuppressWarnings("nullness") // it seems some annotations are missing on Collector.of ... + static Collector, ImmutableSet> collector() { return Collector.of(HashSet::new, Set::add, (set1, set2) -> { set1.addAll(set2); return set1; - }, ImmutableSet::fromSet, Characteristics.UNORDERED); - } - - /** - * Creates an ImmutableSet from a Set. - * - * @param set a Set. - * @return an ImmutableSet containing the same elements as the specified set. - */ - static ImmutableSet fromSet(Set set) { - ImmutableSet result = DefaultImmutableSet.nil(); - - for (T el : set) { - result = result.add(el); - } - - return result; + }, Immutables::createSetFrom, Characteristics.UNORDERED); } /** * Builds a single set with the given obj. */ - static ImmutableSet singleton(T obj) { + static ImmutableSet singleton(T obj) { ImmutableSet result = DefaultImmutableSet.nil(); return result.add(obj); } - static ImmutableSet empty() { + static ImmutableSet empty() { return DefaultImmutableSet.nil(); } - - static ImmutableSet fromCollection(@NonNull Collection seq) { - return fromSet(new HashSet<>(seq)); - } - /** * @return a {@code Set} containing the same elements as this {@code ImmutableSet} */ @@ -115,7 +95,7 @@ static ImmutableSet fromCollection(@NonNull Collection seq) * @return true iff the this set is subset of o and vice versa. */ @Override - boolean equals(Object o); + boolean equals(@Nullable Object o); @Override int hashCode(); diff --git a/key.util/src/main/java/org/key_project/util/collection/Immutables.java b/key.util/src/main/java/org/key_project/util/collection/Immutables.java index 7c9cd4c3919..9dc51e9218e 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Immutables.java +++ b/key.util/src/main/java/org/key_project/util/collection/Immutables.java @@ -4,10 +4,11 @@ package org.key_project.util.collection; import java.util.HashSet; -import java.util.Set; import java.util.function.Function; import java.util.function.Predicate; +import org.jspecify.annotations.Nullable; + /** * This class is a collection of methods that operate on immutable collections, in particular * {@link ImmutableSet}s and {@link ImmutableList}s. @@ -34,8 +35,7 @@ private Immutables() { * @param list any list, must not be null * @return true iff every */ - public static boolean isDuplicateFree(ImmutableList list) { - + public static boolean isDuplicateFree(ImmutableList list) { HashSet set = new HashSet<>(); for (T element : list) { if (set.contains(element)) { @@ -63,7 +63,7 @@ public static boolean isDuplicateFree(ImmutableList list) { * The implementation uses a hash set internally and thus runs in O(n). * * It reuses as much created datastructure as possible. In particular, if the list is already - * duplicate-fre, it does not allocate new memory (well, only temporarily) and returns the + * duplicate-free, it does not allocate new memory (well, only temporarily) and returns the * argument. * * Sidenote: Would that not make a nice KeY-Verification condition? Eat your own dogfood. @@ -72,7 +72,8 @@ public static boolean isDuplicateFree(ImmutableList list) { * * @return a duplicate-free version of the argument, never null */ - public static ImmutableList removeDuplicates(ImmutableList list) { + public static ImmutableList removeDuplicates( + ImmutableList list) { if (list.isEmpty()) { return list; @@ -90,6 +91,7 @@ public static ImmutableList removeDuplicates(ImmutableList list) { while (!stack.isEmpty()) { ImmutableList top = stack.head(); + assert !top.isEmpty() : "@AssumeAssertion(nullness)"; T element = top.head(); stack = stack.tail(); if (alreadySeen.contains(element)) { @@ -102,6 +104,7 @@ public static ImmutableList removeDuplicates(ImmutableList list) { while (!stack.isEmpty()) { ImmutableList top = stack.head(); + assert !top.isEmpty() : "@AssumeAssertion(nullness)"; T element = top.head(); stack = stack.tail(); if (!alreadySeen.contains(element)) { @@ -114,10 +117,11 @@ public static ImmutableList removeDuplicates(ImmutableList list) { } - public static ImmutableList concatDuplicateFreeLists(ImmutableList l1, + public static ImmutableList concatDuplicateFreeLists( + ImmutableList l1, ImmutableList l2) { - Set lookup = new HashSet<>(); + HashSet lookup = new HashSet<>(); for (T element : l1) { lookup.add(element); } @@ -132,7 +136,19 @@ public static ImmutableList concatDuplicateFreeLists(ImmutableList l1, return result; } - public static ImmutableSet createSetFrom(Iterable iterable) { + /** + * Returns an immutable set consisting of the elements of the + * given iterable collection. + * + * The iteration order of the result is identical to that of the argument. + * + * @param iterable the collection to iterate through to obtain the elements + * for the resulting list + * + * @return the view onto the iterable as an immutable set + */ + public static ImmutableSet createSetFrom( + Iterable iterable) { return DefaultImmutableSet.fromImmutableList(createListFrom(iterable)); } @@ -145,9 +161,9 @@ public static ImmutableSet createSetFrom(Iterable iterable) { * @param iterable the collection to iterate through to obtain the elements * for the resulting list * - * @returns the view onto the iterable as an immutable list + * @return the view onto the iterable as an immutable list */ - public static ImmutableList createListFrom(Iterable iterable) { + public static ImmutableList createListFrom(Iterable iterable) { ImmutableList result = ImmutableSLList.nil(); for (T t : iterable) { result = result.prepend(t); @@ -167,11 +183,12 @@ public static ImmutableList createListFrom(Iterable iterable) { * * @returns the filtered list */ - public static ImmutableList filter(ImmutableList ts, Predicate predicate) { + public static ImmutableList filter(ImmutableList ts, + Predicate predicate) { // This must be a loop. A tail recursive implementation is not optimised // by the compiler and quickly leads to a stack overlow. ImmutableList acc = ImmutableSLList.nil(); - while (ts.size() > 0) { + while (!ts.isEmpty()) { T hd = ts.head(); if (predicate.test(hd)) { acc = acc.prepend(hd); @@ -190,11 +207,12 @@ public static ImmutableList filter(ImmutableList ts, Predicate pred * @param function a non-interfering, stateless function to apply to each element * @return the mapped list of the same length as this */ - public static ImmutableList map(ImmutableList ts, Function function) { + public static ImmutableList map( + ImmutableList ts, Function function) { // This must be a loop. A tail recursive implementation is not optimised // by the compiler and quickly leads to a stack overlow. ImmutableList acc = ImmutableSLList.nil(); - while (ts.size() > 0) { + while (!ts.isEmpty()) { T hd = ts.head(); acc = acc.prepend(function.apply(hd)); ts = ts.tail(); diff --git a/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java b/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java index d7e1e6fcc46..e6193c17e99 100644 --- a/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java +++ b/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java @@ -10,10 +10,12 @@ import java.util.stream.Collectors; import java.util.stream.StreamSupport; +import org.checkerframework.checker.nullness.util.NullnessUtil; +import org.jspecify.annotations.Nullable; + /** * Utilities for Collections. * - * * @author Alexander Weigl * @version 1 (29.03.19) */ @@ -27,9 +29,11 @@ public class KeYCollections { * first one. */ public static S[] concat(S[] s1, T[] s2) { + @Nullable S[] res = Arrays.copyOf(s1, s1.length + s2.length); System.arraycopy(s2, 0, res, s1.length, s2.length); - return res; + // After arraycopy, all elements of res are NonNull. + return NullnessUtil.castNonNullDeep(res); } // ======================================================= @@ -58,9 +62,12 @@ public static Map apply(Map m0, Map m1) { } for (Map.Entry e : m0.entrySet()) { - final U value = m1.get(e.getValue()); - if (value != null) { - res.put(e.getKey(), value); + final T v1 = e.getValue(); + if (v1 != null) { + final U value = m1.get(v1); + if (value != null) { + res.put(e.getKey(), value); + } } } return res; diff --git a/key.util/src/main/java/org/key_project/util/collection/NotUniqueException.java b/key.util/src/main/java/org/key_project/util/collection/NotUniqueException.java index fc8748aa286..3d734f450f7 100644 --- a/key.util/src/main/java/org/key_project/util/collection/NotUniqueException.java +++ b/key.util/src/main/java/org/key_project/util/collection/NotUniqueException.java @@ -4,20 +4,19 @@ package org.key_project.util.collection; +import org.jspecify.annotations.Nullable; /** thrown if a duplicate is being added via addUnique() */ public class NotUniqueException extends Exception { + private final @Nullable Object offender; - private static final long serialVersionUID = 6565515240836947955L; - final Object offender; - - public NotUniqueException(Object o) { + public NotUniqueException(@Nullable Object o) { offender = o; } @Override public String toString() { - return "Tried to add a duplicate object to set. Offender is \n" + offender + "\nof class " - + offender.getClass(); + return "Tried to add a duplicate object to set. Offender is \n" + offender + + (offender != null ? " of class " + offender.getClass() : ""); } } diff --git a/key.util/src/main/java/org/key_project/util/collection/Pair.java b/key.util/src/main/java/org/key_project/util/collection/Pair.java index 56cb9295521..29a7d3f9393 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Pair.java +++ b/key.util/src/main/java/org/key_project/util/collection/Pair.java @@ -8,6 +8,8 @@ import java.util.Objects; import java.util.Set; +import org.jspecify.annotations.Nullable; + /** * Simple value object to hold two values. * @@ -43,7 +45,7 @@ public String toString() { @Override - public boolean equals(Object o) { + public boolean equals(@Nullable Object o) { if (!(o instanceof Pair p)) { return false; } diff --git a/key.util/src/main/java/org/key_project/util/collection/PropertiesUtil.java b/key.util/src/main/java/org/key_project/util/collection/PropertiesUtil.java index ac84384ede7..d82b74398e3 100644 --- a/key.util/src/main/java/org/key_project/util/collection/PropertiesUtil.java +++ b/key.util/src/main/java/org/key_project/util/collection/PropertiesUtil.java @@ -10,6 +10,7 @@ import java.nio.charset.StandardCharsets; import java.util.Properties; +@SuppressWarnings("nullness") public class PropertiesUtil { private PropertiesUtil() { diff --git a/key.util/src/main/java/org/key_project/util/collection/package-info.java b/key.util/src/main/java/org/key_project/util/collection/package-info.java new file mode 100644 index 00000000000..06e5b31dba6 --- /dev/null +++ b/key.util/src/main/java/org/key_project/util/collection/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (24.07.23) + */ +@NullMarked +package org.key_project.util.collection; + +import org.jspecify.annotations.NullMarked; diff --git a/key.util/src/main/java/org/key_project/util/helper/FindResources.java b/key.util/src/main/java/org/key_project/util/helper/FindResources.java index 580d0a288d7..64f13ac7efd 100644 --- a/key.util/src/main/java/org/key_project/util/helper/FindResources.java +++ b/key.util/src/main/java/org/key_project/util/helper/FindResources.java @@ -10,9 +10,10 @@ import java.nio.file.*; import java.util.Arrays; import java.util.List; -import java.util.Objects; import java.util.stream.Collectors; +import org.jspecify.annotations.Nullable; + /** * @author Alexander Weigl * @version 1 (13.02.19) @@ -29,13 +30,20 @@ public final class FindResources { * @throws IOException * @author Greg Briggs */ - public static List getResources(String path, Class clazz) + public static @Nullable List getResources(String path, Class clazz) throws URISyntaxException, IOException { - URL dirURL = clazz.getClassLoader().getResource(path); + final var classLoader = clazz.getClassLoader(); + + if (classLoader == null) + return null; + + @Nullable + URL dirURL = classLoader.getResource(path); if (dirURL != null && dirURL.getProtocol().equals("file")) { /* A file path: easy enough */ File[] files = new File(dirURL.toURI()).listFiles(); - Objects.requireNonNull(files); + if (files == null) + files = new File[0]; return Arrays.stream(files).map(File::toPath).collect(Collectors.toList()); } @@ -45,7 +53,7 @@ public static List getResources(String path, Class clazz) * jar as clazz. */ String me = clazz.getName().replace(".", "/") + ".class"; - dirURL = clazz.getClassLoader().getResource(me); + dirURL = classLoader.getResource(me); } if (dirURL == null) { @@ -57,7 +65,7 @@ public static List getResources(String path, Class clazz) // strip out only the JAR file String jarPath = dirURL.getPath().substring(5, dirURL.getPath().indexOf('!')); try (FileSystem fs = - FileSystems.newFileSystem(Paths.get(jarPath), clazz.getClassLoader())) { + FileSystems.newFileSystem(Paths.get(jarPath), classLoader)) { Path dir = fs.getPath(path); try (var s = Files.list(dir)) { return s.collect(Collectors.toList()); @@ -67,13 +75,17 @@ public static List getResources(String path, Class clazz) throw new UnsupportedOperationException("Cannot list files for URL \"" + dirURL + "\""); } - public static List getResources(String path) throws URISyntaxException, IOException { + public static @Nullable List getResources(String path) + throws URISyntaxException, IOException { return getResources(path, FindResources.class); } - public static Path getResource(String path, Class clazz) + public static @Nullable Path getResource(String path, Class clazz) throws URISyntaxException, IOException { - URL dirURL = clazz.getClassLoader().getResource(path); + final var classLoader = clazz.getClassLoader(); + if (classLoader == null) + return null; + URL dirURL = classLoader.getResource(path); if (dirURL != null && dirURL.getProtocol().equals("file")) { return new File(dirURL.toURI()).toPath(); } @@ -84,7 +96,7 @@ public static Path getResource(String path, Class clazz) * jar as clazz. */ String me = clazz.getName().replace(".", "/") + ".class"; - dirURL = clazz.getClassLoader().getResource(me); + dirURL = classLoader.getResource(me); } if (dirURL == null) { @@ -96,14 +108,15 @@ public static Path getResource(String path, Class clazz) // strip out only the JAR file String jarPath = dirURL.getPath().substring(5, dirURL.getPath().indexOf('!')); try (FileSystem fs = - FileSystems.newFileSystem(Paths.get(jarPath), clazz.getClassLoader())) { + FileSystems.newFileSystem(Paths.get(jarPath), classLoader)) { return fs.getPath(path); } } throw new UnsupportedOperationException("Cannot list files for URL \"" + dirURL + "\""); } - public static Path getResource(String path) throws URISyntaxException, IOException { + public static @Nullable Path getResource(String path) + throws URISyntaxException, IOException { return getResource(path, FindResources.class); } @@ -112,7 +125,7 @@ public static Path getResource(String path) throws URISyntaxException, IOExc * @param candidates * @return */ - public static File findFolder(String property, String... candidates) { + public static @Nullable File findFolder(String property, String... candidates) { return findFolder(true, property, candidates); } @@ -131,7 +144,7 @@ public static File findFolder(String property, String... candidates) { * user * @return */ - public static File findFolder(boolean exists, String property, String... candidates) { + public static @Nullable File findFolder(boolean exists, String property, String... candidates) { if (System.getProperty(property) != null) { File f = new File(System.getProperty(property)); if (f.exists() || !exists) { @@ -147,23 +160,23 @@ public static File findFolder(boolean exists, String property, String... candida return null; } - public static File getExampleDirectory() { + public static @Nullable File getExampleDirectory() { return findFolder("KEY_EXAMPLES_DIR", "key.ui/examples", "../key.ui/examples", "examples"); } - public static File getTestResultForRunAllProofs() { + public static @Nullable File getTestResultForRunAllProofs() { return findFolder(false, "KEY_TESTRESULT_RUNALLPROOFS", "build/reports/runallproofs"); } - public static File getTestCasesDirectory() { + public static @Nullable File getTestCasesDirectory() { return findFolder("TEST_CASES", "src/test/resources/testcase"); } - public static File getTestResourcesDirectory() { + public static @Nullable File getTestResourcesDirectory() { return findFolder("TEST_RESOURCES", "src/test/resources/"); } - public static File getTacletProofsDirectory() { + public static @Nullable File getTacletProofsDirectory() { return findFolder("TACLET_PROOFS", "key.core/tacletProofs", "../key.core/tacletProofs", "tacletProofs"); } diff --git a/key.util/src/main/java/org/key_project/util/helper/HelperClassForUtilityTests.java b/key.util/src/main/java/org/key_project/util/helper/HelperClassForUtilityTests.java index 2f5716d9650..176a29171f1 100644 --- a/key.util/src/main/java/org/key_project/util/helper/HelperClassForUtilityTests.java +++ b/key.util/src/main/java/org/key_project/util/helper/HelperClassForUtilityTests.java @@ -8,6 +8,7 @@ import java.io.IOException; import java.nio.charset.StandardCharsets; +@SuppressWarnings("nullness") public class HelperClassForUtilityTests { public static final File RESOURCE_DIRECTORY = FindResources.getTestResourcesDirectory(); diff --git a/key.util/src/main/java/org/key_project/util/helper/package-info.java b/key.util/src/main/java/org/key_project/util/helper/package-info.java new file mode 100644 index 00000000000..3472f55554e --- /dev/null +++ b/key.util/src/main/java/org/key_project/util/helper/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (24.07.23) + */ +@NullMarked +package org.key_project.util.helper; + +import org.jspecify.annotations.NullMarked; diff --git a/key.util/src/main/java/org/key_project/util/java/ArrayUtil.java b/key.util/src/main/java/org/key_project/util/java/ArrayUtil.java index f18e83601c6..c1fe336dd4d 100644 --- a/key.util/src/main/java/org/key_project/util/java/ArrayUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/ArrayUtil.java @@ -8,6 +8,8 @@ import java.util.Objects; import java.util.function.Predicate; +import org.jspecify.annotations.Nullable; + /** * Provides static methods to work with arrays. * @@ -23,20 +25,20 @@ private ArrayUtil() { /** * Searches an element in the given {@link Iterable} instance. * + * Returns the first element that satisfies the predicate. + * * @param array The instance to search in. * @param filter The filter to select an element. * @return The found element or {@code null} if no element was found. */ - public static T search(T[] array, Predicate filter) { + public static @Nullable T search(T[] array, Predicate filter) { T result = null; - if (array != null && filter != null) { - int i = 0; - while (result == null && i < array.length) { - if (filter.test(array[i])) { - result = array[i]; - } - i++; + int i = 0; + while (result == null && i < array.length) { + if (filter.test(array[i])) { + result = array[i]; } + i++; } return result; } @@ -57,32 +59,19 @@ public static T search(T[] array, Predicate filter) { * @throws IllegalArgumentException Both parameters are {@code null}. */ @SuppressWarnings("unchecked") - public static T[] addAll(T[] array, T[] toAdd) { - if (array != null) { - if (toAdd != null) { - T[] result = - (T[]) java.lang.reflect.Array.newInstance(array.getClass().getComponentType(), - array.length + toAdd.length); - System.arraycopy(array, 0, result, 0, array.length); - System.arraycopy(toAdd, 0, result, array.length, toAdd.length); - return result; - } else { - T[] result = (T[]) java.lang.reflect.Array - .newInstance(array.getClass().getComponentType(), array.length); - System.arraycopy(array, 0, result, 0, array.length); - return result; - } - } else { - if (toAdd != null) { - T[] result = (T[]) java.lang.reflect.Array - .newInstance(toAdd.getClass().getComponentType(), toAdd.length); - System.arraycopy(toAdd, 0, result, 0, toAdd.length); - return result; - } else { - throw new IllegalArgumentException( - "Can not create an array if both paramters are null."); - } - } + public static T[] addAll(T[] array, T[] toAdd) { + T[] result = + (T[]) java.lang.reflect.Array.newInstance(getComponentType(array), + array.length + toAdd.length); + System.arraycopy(array, 0, result, 0, array.length); + System.arraycopy(toAdd, 0, result, array.length, toAdd.length); + return result; + } + + private static Class getComponentType(T[] array) { + Class arrayClass = array.getClass(); + assert arrayClass.isArray() : "@AssumeAssertion(nullness): This is always the case"; + return (Class) arrayClass.getComponentType(); } /** @@ -102,28 +91,13 @@ public static T[] addAll(T[] array, T[] toAdd) { * @throws IllegalArgumentException Both parameters are {@code null}. */ @SuppressWarnings("unchecked") - public static T[] addAll(T[] array, T[] toAdd, Class newArrayType) { - if (array != null) { - if (toAdd != null) { - T[] result = (T[]) java.lang.reflect.Array.newInstance(newArrayType, - array.length + toAdd.length); - System.arraycopy(array, 0, result, 0, array.length); - System.arraycopy(toAdd, 0, result, array.length, toAdd.length); - return result; - } else { - T[] result = (T[]) java.lang.reflect.Array.newInstance(newArrayType, array.length); - System.arraycopy(array, 0, result, 0, array.length); - return result; - } - } else { - if (toAdd != null) { - T[] result = (T[]) java.lang.reflect.Array.newInstance(newArrayType, toAdd.length); - System.arraycopy(toAdd, 0, result, 0, toAdd.length); - return result; - } else { - return (T[]) java.lang.reflect.Array.newInstance(newArrayType, 0); - } - } + public static T[] addAll(T[] array, T[] toAdd, + Class newArrayType) { + T[] result = (T[]) java.lang.reflect.Array.newInstance(newArrayType, + array.length + toAdd.length); + System.arraycopy(array, 0, result, 0, array.length); + System.arraycopy(toAdd, 0, result, array.length, toAdd.length); + return result; } /** @@ -142,23 +116,12 @@ public static T[] addAll(T[] array, T[] toAdd, Class newArrayType) { * @throws IllegalArgumentException Both parameters are {@code null}. */ @SuppressWarnings("unchecked") - public static T[] add(T[] array, T toAdd) { - if (array != null) { - T[] result = (T[]) java.lang.reflect.Array - .newInstance(array.getClass().getComponentType(), array.length + 1); - System.arraycopy(array, 0, result, 0, array.length); - result[array.length] = toAdd; - return result; - } else { - if (toAdd != null) { - T[] result = (T[]) java.lang.reflect.Array.newInstance(toAdd.getClass(), 1); - result[0] = toAdd; - return result; - } else { - throw new IllegalArgumentException( - "Can not create an array if both paramters are null."); - } - } + public static T[] add(T[] array, T toAdd) { + T[] result = (T[]) java.lang.reflect.Array + .newInstance(getComponentType(array), array.length + 1); + System.arraycopy(array, 0, result, 0, array.length); + result[array.length] = toAdd; + return result; } /** @@ -172,14 +135,10 @@ public static T[] add(T[] array, T toAdd) { * @return The new created array with one more element. */ public static int[] add(int[] array, int toAdd) { - if (array != null) { - int[] result = new int[array.length + 1]; - System.arraycopy(array, 0, result, 0, array.length); - result[array.length] = toAdd; - return result; - } else { - return new int[] { toAdd }; - } + int[] result = new int[array.length + 1]; + System.arraycopy(array, 0, result, 0, array.length); + result[array.length] = toAdd; + return result; } /** @@ -194,26 +153,15 @@ public static int[] add(int[] array, int toAdd) { * @return The new created array with one more element. */ @SuppressWarnings("unchecked") - public static T[] insert(T[] array, T toInsert, int index) { - if (array != null) { - T[] result = (T[]) java.lang.reflect.Array - .newInstance(array.getClass().getComponentType(), array.length + 1); - if (index >= 1) { - System.arraycopy(array, 0, result, 0, index); - } - result[index] = toInsert; - System.arraycopy(array, index, result, index + 1, array.length - index); - return result; - } else { - if (toInsert != null) { - T[] result = (T[]) java.lang.reflect.Array.newInstance(toInsert.getClass(), 1); - result[0] = toInsert; - return result; - } else { - throw new IllegalArgumentException( - "Can not create an array if array and element to insert are null."); - } + public static T[] insert(T[] array, T toInsert, int index) { + T[] result = (T[]) java.lang.reflect.Array + .newInstance(getComponentType(array), array.length + 1); + if (index >= 1) { + System.arraycopy(array, 0, result, 0, index); } + result[index] = toInsert; + System.arraycopy(array, index, result, index + 1, array.length - index); + return result; } /** @@ -225,7 +173,7 @@ public static T[] insert(T[] array, T toInsert, int index) { * @return {@code true} if the array contains the element or {@code false} if not or if the * array is {@code null}. */ - public static boolean contains(T[] array, T toSearch) { + public static boolean contains(T[] array, T toSearch) { return indexOf(array, toSearch) >= 0; } @@ -238,13 +186,11 @@ public static boolean contains(T[] array, T toSearch) { * @return The first index in the array that contains the element to search or {@code -1} if the * elment is not containd in the array. */ - public static int indexOf(T[] array, T toSearch) { + public static int indexOf(T[] array, T toSearch) { int index = -1; - if (array != null) { - for (int i = 0; i < array.length; i++) { - if (Objects.equals(array[i], toSearch)) { - return i; - } + for (int i = 0; i < array.length; i++) { + if (Objects.equals(array[i], toSearch)) { + return i; } } return index; @@ -256,23 +202,18 @@ public static int indexOf(T[] array, T toSearch) { * * @param array The array to remove from. * @param toRemove The element to remove. - * @return A copy of the array without the element toRemove or {@code null} if the given array - * was {@code null}. + * @return A copy of the array without the element toRemove. */ @SuppressWarnings("unchecked") - public static T[] remove(T[] array, T toRemove) { - if (array != null) { - List result = new LinkedList<>(); - for (T element : array) { - if (!Objects.equals(element, toRemove)) { - result.add(element); - } + public static T[] remove(T[] array, T toRemove) { + List result = new LinkedList<>(); + for (T element : array) { + if (!Objects.equals(element, toRemove)) { + result.add(element); } - return result.toArray((T[]) java.lang.reflect.Array - .newInstance(array.getClass().getComponentType(), result.size())); - } else { - return null; } + return (T[]) result.toArray((T[]) java.lang.reflect.Array + .newInstance(getComponentType(array), result.size())); } /** @@ -281,7 +222,7 @@ public static T[] remove(T[] array, T toRemove) { * @param array The array to convert. * @return The array as {@link String}. */ - public static String toString(T[] array) { + public static String toString(T[] array) { return toString(array, ", "); } @@ -292,18 +233,16 @@ public static String toString(T[] array) { * @param separator The separator between to array elements. * @return The array as {@link String}. */ - public static String toString(T[] array, String separator) { + public static String toString(T[] array, String separator) { StringBuilder sb = new StringBuilder(); - if (array != null) { - boolean afterFirst = false; - for (T element : array) { - if (afterFirst) { - sb.append(separator); - } else { - afterFirst = true; - } - sb.append(element); + boolean afterFirst = false; + for (T element : array) { + if (afterFirst) { + sb.append(separator); + } else { + afterFirst = true; } + sb.append(element); } return sb.toString(); } @@ -327,16 +266,14 @@ public static String toString(int[] array) { */ public static String toString(int[] array, String separator) { StringBuilder sb = new StringBuilder(); - if (array != null) { - boolean afterFirst = false; - for (int element : array) { - if (afterFirst) { - sb.append(separator); - } else { - afterFirst = true; - } - sb.append(element); + boolean afterFirst = false; + for (int element : array) { + if (afterFirst) { + sb.append(separator); + } else { + afterFirst = true; } + sb.append(element); } return sb.toString(); } @@ -347,7 +284,7 @@ public static String toString(int[] array, String separator) { * @param array The array to check. * @return {@code true} array is empty or {@code null}, {@code false} array is not empty. */ - public static boolean isEmpty(T[] array) { - return array == null || array.length == 0; + public static boolean isEmpty(T[] array) { + return array.length == 0; } } diff --git a/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java b/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java index c6e462cb99e..baa70c6c94f 100644 --- a/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java @@ -6,6 +6,8 @@ import java.util.*; import java.util.function.Predicate; +import org.jspecify.annotations.Nullable; + /** * Provides static methods to work with {@link Collection}s. * @@ -30,23 +32,19 @@ private CollectionUtil() { * @param toSearch The element to search. * @return The index of the element or {@code -1} if it was not found. */ - public static int indexOf(Iterator iter, T toSearch) { - if (iter != null) { - int i = 0; - boolean found = false; - while (!found && iter.hasNext()) { - T next = iter.next(); - if (Objects.equals(next, toSearch)) { - found = true; - } else { - i++; - } - } - if (found) { - return i; + public static int indexOf(Iterator iter, T toSearch) { + int i = 0; + boolean found = false; + while (!found && iter.hasNext()) { + T next = iter.next(); + if (Objects.equals(next, toSearch)) { + found = true; } else { - return -1; + i++; } + } + if (found) { + return i; } else { return -1; } @@ -72,42 +70,20 @@ public static String toString(Collection collection) { */ public static String toString(Collection collection, String separator) { StringBuilder sb = new StringBuilder(); - if (collection != null) { - boolean afterFirst = false; - for (Object object : collection) { - if (afterFirst) { - if (separator != null) { - sb.append(separator); - } - } else { - afterFirst = true; + boolean afterFirst = false; + for (Object object : collection) { + if (afterFirst) { + if (separator != null) { + sb.append(separator); } - sb.append(object); + } else { + afterFirst = true; } + sb.append(object); } return sb.toString(); } - /** - * Nullpointersave execution of {@link Collection#isEmpty()}. - * - * @param collection The given {@link Collection}. - * @return {@code true} = is empty or {@code null}, {@code false} = is not empty. - */ - public static boolean isEmpty(Collection collection) { - return collection == null || collection.isEmpty(); - } - - /** - * Nullpointersave execution of {@link Map#isEmpty()}. - * - * @param map The given {@link Map}. - * @return {@code true} = is empty or {@code null}, {@code false} = is not empty. - */ - public static boolean isEmpty(Map map) { - return map == null || map.isEmpty(); - } - /** * Adds all elements to the {@link Collection}. * @@ -116,10 +92,8 @@ public static boolean isEmpty(Map map) { * @param iterable The elements to add. */ public static void addAll(Collection collection, Iterable iterable) { - if (collection != null && iterable != null) { - for (T toAdd : iterable) { - collection.add(toAdd); - } + for (T toAdd : iterable) { + collection.add(toAdd); } } @@ -131,20 +105,17 @@ public static void addAll(Collection collection, Iterable iterable) { * @return {@code true} if at least one element was removed, {@code false} if the * {@link Collection} was not modified. */ - public static boolean removeComplete(Collection collection, T toRemove) { - if (collection != null) { - Iterator iter = collection.iterator(); - boolean changed = false; - while (iter.hasNext()) { - if (Objects.equals(iter.next(), toRemove)) { - iter.remove(); - changed = true; - } + public static boolean removeComplete(Collection collection, + T toRemove) { + Iterator iter = collection.iterator(); + boolean changed = false; + while (iter.hasNext()) { + if (Objects.equals(iter.next(), toRemove)) { + iter.remove(); + changed = true; } - return changed; - } else { - return false; } + return changed; } /** @@ -154,13 +125,12 @@ public static boolean removeComplete(Collection collection, T toRemove) { * @param filter The {@link IFilter} to use. * @return The elements accepted by the given {@link Predicate}. */ - public static List searchAll(Iterable iterable, Predicate filter) { + public static List searchAll(Iterable iterable, + Predicate filter) { List result = new ArrayList<>(); - if (iterable != null && filter != null) { - for (T element : iterable) { - if (filter.test(element)) { - result.add(element); - } + for (T element : iterable) { + if (filter.test(element)) { + result.add(element); } } return result; @@ -173,15 +143,14 @@ public static List searchAll(Iterable iterable, Predicate filter) { * @param filter The filter to select an element. * @return The found element or {@code null} if no element was found. */ - public static T search(Iterable iterable, Predicate filter) { + public static @Nullable T search(Iterable iterable, + Predicate filter) { T result = null; - if (iterable != null && filter != null) { - Iterator iter = iterable.iterator(); - while (result == null && iter.hasNext()) { - T next = iter.next(); - if (filter.test(next)) { - result = next; - } + Iterator iter = iterable.iterator(); + while (result == null && iter.hasNext()) { + T next = iter.next(); + if (filter.test(next)) { + result = next; } } return result; @@ -195,16 +164,15 @@ public static T search(Iterable iterable, Predicate filter) { * @param filter The filter to select an element. * @return The found element or {@code null} if no element was found. */ - public static T searchAndRemove(Iterable iterable, Predicate filter) { + public static @Nullable T searchAndRemove(Iterable iterable, + Predicate filter) { T result = null; - if (iterable != null && filter != null) { - Iterator iter = iterable.iterator(); - while (result == null && iter.hasNext()) { - T next = iter.next(); - if (filter.test(next)) { - result = next; - iter.remove(); - } + Iterator iter = iterable.iterator(); + while (result == null && iter.hasNext()) { + T next = iter.next(); + if (filter.test(next)) { + result = next; + iter.remove(); } } return result; @@ -218,17 +186,16 @@ public static T searchAndRemove(Iterable iterable, Predicate filter) { * @param filter The filter to select an element. * @return The found element or {@code null} if no element was found. */ - public static T searchAndRemoveWithException(Iterable iterable, + public static @Nullable T searchAndRemoveWithException( + Iterable iterable, IFilterWithException filter) throws E { T result = null; - if (iterable != null && filter != null) { - Iterator iter = iterable.iterator(); - while (result == null && iter.hasNext()) { - T next = iter.next(); - if (filter.select(next)) { - result = next; - iter.remove(); - } + Iterator iter = iterable.iterator(); + while (result == null && iter.hasNext()) { + T next = iter.next(); + if (filter.select(next)) { + result = next; + iter.remove(); } } return result; @@ -241,13 +208,11 @@ public static T searchAndRemoveWithException(Iterable boolean contains(Iterable iterable, T element) { + public static boolean contains(Iterable iterable, T element) { boolean found = false; - if (iterable != null) { - Iterator iter = iterable.iterator(); - while (!found && iter.hasNext()) { - found = Objects.equals(iter.next(), element); - } + Iterator iter = iterable.iterator(); + while (!found && iter.hasNext()) { + found = Objects.equals(iter.next(), element); } return found; } @@ -260,13 +225,12 @@ public static boolean contains(Iterable iterable, T element) { * @param filter The {@link IFilter} to select elements. * @return The number of elements selected by the {@link IFilter} in the given {@link Iterable}. */ - public static int count(Iterable iterable, Predicate filter) { + public static int count(Iterable iterable, + Predicate filter) { int count = 0; - if (iterable != null && filter != null) { - for (T element : iterable) { - if (filter.test(element)) { - count++; - } + for (T element : iterable) { + if (filter.test(element)) { + count++; } } return count; @@ -285,26 +249,23 @@ public static int count(Iterable iterable, Predicate filter) { * @return {@code true} both {@link Collection}s contains same elements, {@code false} * {@link Collection}s are different. */ - public static boolean containsSame(Collection first, Collection second) { - if (first != null) { - if (second != null) { - if (first.size() == second.size()) { - Collection firstCopy = new LinkedList<>(first); - boolean same = true; - Iterator secondIter = second.iterator(); - while (same && secondIter.hasNext()) { - T secondNext = secondIter.next(); - same = firstCopy.remove(secondNext); - } - return same; - } else { - return false; - } - } else { - return first.size() == 0; + @SuppressWarnings("nullness:argument.type.incompatible") + // Checker Framework conservatively disallows passing null to Collection.remove, but if we have + // a collection of type + // Collection<@Nullable C>, it's probably fine. + public static boolean containsSame(Collection first, + Collection second) { + if (first.size() == second.size()) { + Collection firstCopy = new LinkedList<>(first); + boolean same = true; + Iterator secondIter = second.iterator(); + while (same && secondIter.hasNext()) { + T secondNext = secondIter.next(); + same = firstCopy.remove(secondNext); } + return same; } else { - return second == null || second.size() == 0; + return false; } } @@ -314,16 +275,12 @@ public static boolean containsSame(Collection first, Collection second * @param iterable The {@link Iterable} to remove first element from. * @return The removed first element or {@code null} if no element was removed. */ - public static T removeFirst(Iterable iterable) { + public static @Nullable T removeFirst(Iterable iterable) { try { - if (iterable != null) { - Iterator iter = iterable.iterator(); - T next = iter.next(); - iter.remove(); - return next; - } else { - return null; - } + Iterator iter = iterable.iterator(); + T next = iter.next(); + iter.remove(); + return next; } catch (NoSuchElementException e) { return null; // Iterable must be empty. } @@ -336,7 +293,8 @@ public static T removeFirst(Iterable iterable) { * @param toInsert The element to insert. * @param comparator The {@link Comparator} to use. */ - public static void binaryInsert(List list, T toInsert, Comparator comparator) { + public static void binaryInsert(List list, T toInsert, + Comparator comparator) { if (list.isEmpty()) { list.add(toInsert); } else { diff --git a/key.util/src/main/java/org/key_project/util/java/IFilterWithException.java b/key.util/src/main/java/org/key_project/util/java/IFilterWithException.java index db96031f16e..5eb8eeb4a92 100644 --- a/key.util/src/main/java/org/key_project/util/java/IFilterWithException.java +++ b/key.util/src/main/java/org/key_project/util/java/IFilterWithException.java @@ -3,13 +3,15 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.java; +import org.jspecify.annotations.Nullable; + /** * Utility class to select elements which also allows that exceptions are thrown during selection * phase. * * @author Martin Hentschel */ -public interface IFilterWithException { +public interface IFilterWithException { /** * Checks if the given element should be selected. * diff --git a/key.util/src/main/java/org/key_project/util/java/IOUtil.java b/key.util/src/main/java/org/key_project/util/java/IOUtil.java index 39fe82a3581..65578b4e82a 100644 --- a/key.util/src/main/java/org/key_project/util/java/IOUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/IOUtil.java @@ -16,6 +16,9 @@ import java.util.zip.ZipException; import java.util.zip.ZipInputStream; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * Provides static methods to work with java IO. * @@ -43,7 +46,7 @@ private IOUtil() { * * @return The home directory. */ - public static File getHomeDirectory() { + public static @Nullable File getHomeDirectory() { String path = System.getProperty("user.home"); if (path != null) { return new File(path); @@ -58,15 +61,11 @@ public static File getHomeDirectory() { * @param file The file to extract it extension. * @return The file extension or {@code null} if not available. */ - public static String getFileExtension(File file) { - if (file != null) { - String name = file.getName(); - int dotIndex = name.lastIndexOf('.'); - if (dotIndex >= 0) { - return name.substring(dotIndex + 1); - } else { - return null; - } + public static @Nullable String getFileExtension(File file) { + String name = file.getName(); + int dotIndex = name.lastIndexOf('.'); + if (dotIndex >= 0) { + return name.substring(dotIndex + 1); } else { return null; } @@ -77,18 +76,14 @@ public static String getFileExtension(File file) { * * @param fileName The file name with extension for that the file name without extension is * needed. - * @return The file name without extension or {@code null} if it was not possible to compute it. + * @return The file name without extension. */ public static String getFileNameWithoutExtension(String fileName) { - if (fileName != null) { - int dotIndex = fileName.lastIndexOf('.'); - if (dotIndex >= 0) { - return fileName.substring(0, dotIndex); - } else { - return fileName; - } + int dotIndex = fileName.lastIndexOf('.'); + if (dotIndex >= 0) { + return fileName.substring(0, dotIndex); } else { - return null; + return fileName; } } @@ -98,7 +93,7 @@ public static String getFileNameWithoutExtension(String fileName) { * @param file The file/folder to delete. */ public static void delete(File file) { - if (file != null && file.exists()) { + if (file.exists()) { if (file.isDirectory()) { File[] children = file.listFiles(); if (children != null) { @@ -118,12 +113,8 @@ public static void delete(File file) { * @return The read content or {@code null} if the {@link URL} is {@code null}. * @throws IOException Occurred Exception. */ - public static Optional readFrom(URL url) throws IOException { - if (url != null) { - return Optional.of(readFrom(url.openStream())); - } else { - return Optional.empty(); - } + public static @Nullable String readFrom(URL url) throws IOException { + return readFrom(url.openStream()); } /** @@ -133,24 +124,19 @@ public static Optional readFrom(URL url) throws IOException { * @return The read content or {@code null} if the {@link URL} is {@code null}. * @throws IOException Occurred Exception. */ - public static Optional readFrom(URI url) throws IOException { - if (url != null) { - return Optional.of(readFrom(url.toURL().openStream())); - } else { - return Optional.empty(); - } + public static @Nullable String readFrom(URI url) throws IOException { + return readFrom(url.toURL().openStream()); } /** * Reads the complete content from the {@link File}. * * @param file The {@link File} to read from. - * @return The read content or {@code null} if the {@link File} is {@code null} or not an - * existing file. + * @return The read content or {@code null} if the {@link File} is not an existing file. * @throws IOException Occurred Exception. */ - public static String readFrom(File file) throws IOException { - if (file != null && file.isFile()) { + public static @Nullable String readFrom(File file) throws IOException { + if (file.isFile()) { return readFrom(new FileInputStream(file)); } else { return null; @@ -161,14 +147,10 @@ public static String readFrom(File file) throws IOException { * Reads the complete content from the {@link InputStream} and closes it. * * @param in The {@link InputStream} to read from and to close. - * @return The read content or {@code null} if the {@link InputStream} is {@code null}. + * @return The read content. * @throws IOException Occurred Exception. */ public static String readFrom(InputStream in) throws IOException { - if (in == null) { - return null; - } - try (InputStreamReader reader = new InputStreamReader(in, StandardCharsets.UTF_8)) { StringBuilder sb = new StringBuilder(); char[] buffer = new char[BUFFER_SIZE]; @@ -189,7 +171,7 @@ public static String readFrom(InputStream in) throws IOException { * @throws IOException Occurred Exception. */ public static void writeTo(OutputStream out, String content) throws IOException { - writeTo(out, content, (String) null); + writeTo(out, content, DEFAULT_CHARSET); } /** @@ -202,7 +184,7 @@ public static void writeTo(OutputStream out, String content) throws IOException */ public static void writeTo(OutputStream out, String content, Charset encoding) throws IOException { - writeTo(out, content, encoding != null ? encoding.displayName() : null); + writeTo(out, content, encoding.displayName()); } /** @@ -216,13 +198,7 @@ public static void writeTo(OutputStream out, String content, Charset encoding) */ public static void writeTo(OutputStream out, String content, String encoding) throws IOException { - if (out == null || content == null) { - return; - } - - try (PrintStream printStream = - encoding != null ? new PrintStream(out, false, encoding) - : new PrintStream(out, false, DEFAULT_CHARSET)) { + try (PrintStream printStream = new PrintStream(out, false, encoding)) { printStream.print(content); } } @@ -260,11 +236,7 @@ public static void writeTo(OutputStream out, String content, String encoding) * @throws IOException Occurred Exception. */ public static LineInformation[] computeLineInformation(File file) throws IOException { - if (file != null) { - return computeLineInformation(new FileInputStream(file)); - } else { - return computeLineInformation((InputStream) null); - } + return computeLineInformation(new FileInputStream(file)); } /** @@ -299,11 +271,8 @@ public static LineInformation[] computeLineInformation(File file) throws IOExcep * @return The computed start indices. * @throws IOException Occurred Exception. */ - public static LineInformation[] computeLineInformation(InputStream in) throws IOException { - if (in == null) { - return new LineInformation[0]; - } - + public static LineInformation[] computeLineInformation(InputStream in) + throws IOException { try (InputStreamReader reader = new InputStreamReader(in, StandardCharsets.UTF_8)) { List result = new LinkedList<>(); char[] buffer = new char[BUFFER_SIZE]; // Buffer with the read signs @@ -541,13 +510,11 @@ public static File createTempDirectory(String prefix, String suffix) throws IOEx */ public static List search(File file, final Predicate filter) throws IOException { final List result = new LinkedList<>(); - if (file != null) { - visit(file, visitedFile -> { - if (filter == null || filter.test(visitedFile)) { - result.add(visitedFile); - } - }); - } + visit(file, visitedFile -> { + if (filter == null || filter.test(visitedFile)) { + result.add(visitedFile); + } + }); return result; } @@ -559,13 +526,11 @@ public static List search(File file, final Predicate filter) throws * @throws IOException Occurred Exception */ public static void visit(File file, IFileVisitor visitor) throws IOException { - if (file != null && visitor != null) { - visitor.visit(file); - File[] children = file.listFiles(); - if (children != null) { - for (File child : children) { - visit(child, visitor); - } + visitor.visit(file); + File[] children = file.listFiles(); + if (children != null) { + for (File child : children) { + visit(child, visitor); } } } @@ -592,15 +557,12 @@ public interface IFileVisitor { * @return A new {@link InputStream} with with the replaced line breaks. * @throws IOException Occurred Exception. */ - public static InputStream unifyLineBreaks(InputStream in) throws IOException { - if (in != null) { - String text = IOUtil.readFrom(in); - text = text.replace("\r\n", "\n"); - text = text.replace("\r", "\n"); - return new ByteArrayInputStream(text.getBytes(StandardCharsets.UTF_8)); - } else { - return null; - } + public static InputStream unifyLineBreaks(InputStream in) + throws IOException { + String text = IOUtil.readFrom(in); + text = text.replace("\r\n", "\n"); + text = text.replace("\r", "\n"); + return new ByteArrayInputStream(text.getBytes(StandardCharsets.UTF_8)); } /** @@ -632,13 +594,13 @@ public static boolean contains(Iterable parents, File child) { */ public static boolean contains(File parent, File child) { boolean contains = false; - if (parent != null && child != null) { - while (!contains && child != null) { - if (parent.equals(child)) { - contains = true; - } - child = child.getParentFile(); + @Nullable + File current = child; + while (!contains && current != null) { + if (parent.equals(current)) { + contains = true; } + current = current.getParentFile(); } return contains; } @@ -653,25 +615,16 @@ public static boolean contains(File parent, File child) { */ public static boolean copy(Reader source, StringWriter target) throws IOException { try { - if (source != null && target != null) { - char[] buffer = new char[BUFFER_SIZE]; - int read; - while ((read = source.read(buffer)) >= 1) { - target.write(buffer, 0, read); - } - return true; - } else { - return false; + char[] buffer = new char[BUFFER_SIZE]; + int read; + while ((read = source.read(buffer)) >= 1) { + target.write(buffer, 0, read); } + return true; } finally { - if (source != null) { - source.close(); - } - if (target != null) { - target.close(); - } + source.close(); + target.close(); } - } /** @@ -685,65 +638,43 @@ public static boolean copy(Reader source, StringWriter target) throws IOExceptio */ public static boolean copy(InputStream source, OutputStream target) throws IOException { try { - if (source != null && target != null) { - byte[] buffer = new byte[BUFFER_SIZE]; - int read; - while ((read = source.read(buffer)) >= 1) { - target.write(buffer, 0, read); - } - return true; - } else { - return false; + byte[] buffer = new byte[BUFFER_SIZE]; + int read; + while ((read = source.read(buffer)) >= 1) { + target.write(buffer, 0, read); } + return true; } finally { - if (source != null) { - source.close(); - } - if (target != null) { - target.close(); - } + source.close(); + target.close(); } } - /** - * Checks if the given {@link File} exists. - * - * @param file The {@link File} to check. - * @return {@code true} {@link File} is not {@code null} and exists, {@code false} otherwise. - */ - public static boolean exists(File file) { - return file != null && file.exists(); - } - - public static URL getClassLocationURL(Class classInstance) { + public static @Nullable URL getClassLocationURL(Class classInstance) { CodeSource cs = classInstance.getProtectionDomain().getCodeSource(); return cs != null ? cs.getLocation() : null; } - public static File getClassLocation(Class classInstance) { - if (classInstance != null) { - return toFile(getClassLocationURL(classInstance)); - } else { - return null; - } + public static @Nullable File getClassLocation(Class classInstance) { + return toFile(getClassLocationURL(classInstance)); } - public static File getProjectRoot(Class classInstance) { + public static @Nullable File getProjectRoot(Class classInstance) { File file = getClassLocation(classInstance); return file != null ? file.getParentFile() : null; } - public static File toFile(URL url) { + public static @Nullable File toFile(@Nullable URL url) { URI uri = toURI(url); return uri != null ? new File(uri) : null; } - public static String toFileString(URL url) { + public static @Nullable String toFileString(@Nullable URL url) { File file = toFile(url); return file != null ? file.toString() : null; } - public static URI toURI(URL url) { + public static @Nullable URI toURI(@Nullable URL url) { try { if (url != null) { String protocol = url.getProtocol(); @@ -774,7 +705,10 @@ public static URI toURI(URL url) { * @return The current directory. */ public static File getCurrentDirectory() { - return new File(".").getAbsoluteFile().getParentFile(); + File result = new File(".").getAbsoluteFile().getParentFile(); + assert result != null + : "@AssumeAssertion(nullness): this always works, even in the toplevel directory ..."; + return result; } /** @@ -839,7 +773,12 @@ public static void extractZip(InputStream in, Path targetDir) throws IOException Files.createDirectories(path); } else { // create nonexistent parent directories and then extract the file - Files.createDirectories(path.getParent()); + // Since path is the result of resolving a zip entry name in the + // target directory, it does have a parent. + @SuppressWarnings("nullness") + @NonNull + Path parent = path.getParent(); + Files.createDirectories(parent); Files.copy(zin, path); } } diff --git a/key.util/src/main/java/org/key_project/util/java/IntegerUtil.java b/key.util/src/main/java/org/key_project/util/java/IntegerUtil.java index cd5ee659ab6..240bc59f135 100644 --- a/key.util/src/main/java/org/key_project/util/java/IntegerUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/IntegerUtil.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.java; + public final class IntegerUtil { /** * Forbid instances. diff --git a/key.util/src/main/java/org/key_project/util/java/MapUtil.java b/key.util/src/main/java/org/key_project/util/java/MapUtil.java index b9ad2689b75..bdabc94c6b9 100644 --- a/key.util/src/main/java/org/key_project/util/java/MapUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/MapUtil.java @@ -15,6 +15,7 @@ * * @author lanzinger */ +@SuppressWarnings("nullness") public final class MapUtil { private MapUtil() {} diff --git a/key.util/src/main/java/org/key_project/util/java/NumberUtil.java b/key.util/src/main/java/org/key_project/util/java/NumberUtil.java index f08710f645f..bbf2c637d99 100644 --- a/key.util/src/main/java/org/key_project/util/java/NumberUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/NumberUtil.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.java; + /** * Provides utility methods to work with numbers. * diff --git a/key.util/src/main/java/org/key_project/util/java/StringUtil.java b/key.util/src/main/java/org/key_project/util/java/StringUtil.java index e265e58c67e..710c322e5d6 100644 --- a/key.util/src/main/java/org/key_project/util/java/StringUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/StringUtil.java @@ -6,10 +6,13 @@ import java.util.Arrays; import java.util.Comparator; import java.util.function.Predicate; +import java.util.regex.Matcher; import java.util.regex.Pattern; import javax.swing.*; +import org.checkerframework.checker.nullness.qual.PolyNull; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** * Provides static methods to work with strings. @@ -76,7 +79,7 @@ private StringUtil() { * @param text The text to check. * @return {@code true} = text is {@code null} or empty, {@code false} = text is not empty. */ - public static boolean isEmpty(String text) { + public static boolean isEmpty(@Nullable String text) { return text == null || text.isEmpty(); } @@ -87,7 +90,7 @@ public static boolean isEmpty(String text) { * @return {@code true} = text is {@code null} or trimmed empty, {@code false} = text is not * empty. */ - public static boolean isTrimmedEmpty(String text) { + public static boolean isTrimmedEmpty(@Nullable String text) { return text == null || text.trim().isEmpty(); } @@ -97,7 +100,7 @@ public static boolean isTrimmedEmpty(String text) { * @param text The text. * @return The trimmed text. */ - public static String trim(String text) { + public static @Nullable String trim(@Nullable String text) { return text != null ? text.trim() : null; } @@ -107,8 +110,8 @@ public static String trim(String text) { * @param text The text to convert. * @return The text in lower case or {@code null} if the given text is {@code null}. */ - public static String toLowerCase(String text) { - return text != null ? text.toLowerCase() : null; + public static @PolyNull String toLowerCase(@PolyNull String text) { + return text == null ? null : text.toLowerCase(); } /** @@ -120,7 +123,7 @@ public static String toLowerCase(String text) { * * @return The created {@link Comparator}. */ - public static Comparator createIgnoreCaseComparator() { + public static Comparator<@Nullable String> createIgnoreCaseComparator() { return (o1, o2) -> { if (o1 != null && o2 != null) { return o1.compareToIgnoreCase(o2); @@ -155,7 +158,7 @@ public static String repeat(String text, int repetitions) { * {@code false} if at least one string is {@code null} or the string does not contain * the substring. */ - public static boolean contains(String string, CharSequence substring) { + public static boolean contains(@Nullable String string, @Nullable CharSequence substring) { return string != null && substring != null && string.contains(substring); } @@ -170,7 +173,7 @@ public static boolean contains(String string, CharSequence substring) { * * @author Mattias Ulbrich (under GPL) */ - public static String wrapLines(String string, int length) { + public static @NonNull String wrapLines(@NonNull String string, int length) { char[] c = string.toCharArray(); WrapUtils.wrapLines(c, length); return new String(c); @@ -186,7 +189,7 @@ public static String wrapLines(String string, int length) { * * @author Mattias Ulbrich (under GPL) */ - public static String wrapLines(String string) { + public static @NonNull String wrapLines(@NonNull String string) { return wrapLines(string, 100); } @@ -197,7 +200,7 @@ public static String wrapLines(String string) { * @param text The text to convert. * @return The single lined text. */ - public static String toSingleLinedString(String text) { + public static @Nullable String toSingleLinedString(@Nullable String text) { return replaceAll(text, new char[] { '\n', '\r', '\t' }, ' '); } @@ -209,7 +212,8 @@ public static String toSingleLinedString(String text) { * @param toReplace The sign to replace with. * @return The new created {@link String}. */ - public static String replaceAll(String text, char[] toSearch, char toReplace) { + public static @Nullable String replaceAll(@Nullable String text, char[] toSearch, + char toReplace) { if (text != null && toSearch != null) { // Sort toSearch Arrays.sort(toSearch); @@ -234,7 +238,7 @@ public static String replaceAll(String text, char[] toSearch, char toReplace) { * @param second The second {@link String}. * @return {@code true} equal ignoring whitespace, {@code false} different. */ - public static boolean equalIgnoreWhiteSpace(String first, String second) { + public static boolean equalIgnoreWhiteSpace(@Nullable String first, @Nullable String second) { if (first != null) { if (second != null) { char[] firstContent = first.toCharArray(); @@ -297,7 +301,8 @@ && contains(WHITESPACE, secondContent[secondIndex] + EMPTY_STRING)) { * @return The created text. * @throws IllegalArgumentException If the text is already longer as the given length */ - public static String fillString(String text, char leadingCharacter, int length) + public static @NonNull String fillString(@Nullable String text, char leadingCharacter, + int length) throws IllegalArgumentException { StringBuilder sb = new StringBuilder(); if (text != null) { @@ -320,7 +325,7 @@ public static String fillString(String text, char leadingCharacter, int length) * @param text The text to trim its right side. * @return The trimmed text. */ - public static String trimRight(String text) { + public static @PolyNull String trimRight(@PolyNull String text) { if (text != null) { char[] content = text.toCharArray(); int newLength = content.length; @@ -340,7 +345,7 @@ public static String trimRight(String text) { * @param maxLength The maximal length to ensure. * @return The text considering the maximal length. */ - public static String chop(String text, int maxLength) { + public static @PolyNull String chop(@PolyNull String text, int maxLength) { if (text != null && text.length() > maxLength) { if (maxLength <= 0) { return EMPTY_STRING; @@ -366,11 +371,11 @@ public static String chop(String text, int maxLength) { * @return {@code true} {@link Object} is {@link String} with given prefix, {@code false} * otherwise. */ - public static boolean startsWith(Object obj, String prefix) { + public static boolean startsWith(@Nullable Object obj, @Nullable String prefix) { return obj instanceof String && prefix != null && ((String) obj).startsWith(prefix); } - public static boolean isNumber(String val) { + public static boolean isNumber(@NonNull String val) { try { Long.parseLong(val); } catch (NumberFormatException e) { @@ -387,8 +392,8 @@ public static boolean isNumber(String val) { * * The given predicate test the characters, if true the character is removed. */ - @NonNull - public static String trim(@NonNull String text, @NonNull Predicate predicate) { + public static @NonNull String trim(@NonNull String text, + @NonNull Predicate predicate) { int first = 0; int last = text.length() - 1; char[] value = text.toCharArray(); @@ -407,8 +412,7 @@ public static String trim(@NonNull String text, @NonNull Predicate pr * * @see #trim(String, Predicate) */ - @NonNull - public static String trim(String text, char c) { + public static @NonNull String trim(@NonNull String text, char c) { return trim(text, it -> it == c); } @@ -417,8 +421,7 @@ public static String trim(String text, char c) { * * @see #trim(String, Predicate) */ - @NonNull - public static String trim(String text, String chars) { + public static @NonNull String trim(@NonNull String text, @NonNull String chars) { return trim(text, it -> chars.indexOf(it) >= 0); } @@ -429,10 +432,50 @@ public static String trim(String text, String chars) { * @param with with * @return the normalized text. */ - public static String replaceNewlines(String text, String with) { + public static @NonNull String replaceNewlines(@NonNull String text, String with) { return NEWLINE_PATTERN.matcher(text).replaceAll(with); } + /** + * Checks whether a string contains another one as a whole word (i.e., separated by whitespaces + * or a semicolon at the end). + * + * @param s string to search in + * @param word string to be searched for + */ + public static boolean containsWholeWord(@NonNull String s, @NonNull String word) { + Pattern p = Pattern.compile("\\b" + word + "\\b"); + Matcher m = p.matcher(s); + return m.find(); + /* + * if (s == null || word == null) { return false; } int i = -1; final int wl = + * word.length(); while (true) { i = s.indexOf(word, i + 1); if (i < 0 || i >= s.length()) + * break; if (i == 0 || Character.isWhitespace(s.charAt(i - 1))) { if (i + wl == s.length() + * || Character.isWhitespace(s.charAt(i + wl)) || s.charAt(i + wl) == ';') { return true; } + * } } return false; + */ + } + + /** + * There are different kinds of JML markers. See Section 4.4 "Annotation markers" of the JML + * reference manual. + * + * @param comment + * @return + */ + public static boolean isJMLComment(@NonNull String comment) { + try { + return (comment.startsWith("/*@") || comment.startsWith("//@") + || comment.startsWith("/*+KeY@") || comment.startsWith("//+KeY@") + || (comment.startsWith("/*-") && !comment.startsWith("KeY", 3) + && comment.contains("@")) + || (comment.startsWith("//-") && !comment.startsWith("KeY", 3) + && comment.contains("@"))); + } catch (IndexOutOfBoundsException e) { + return false; + } + } + /** * Count occurences of character x in text, starting at beginIndex and ending at endIndex * (exclusive). diff --git a/key.util/src/main/java/org/key_project/util/java/XMLUtil.java b/key.util/src/main/java/org/key_project/util/java/XMLUtil.java index 78aa587411c..0a3b5022dec 100644 --- a/key.util/src/main/java/org/key_project/util/java/XMLUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/XMLUtil.java @@ -6,6 +6,8 @@ import java.util.Map; import java.util.Map.Entry; +import org.jspecify.annotations.Nullable; + /** * Provides static methods to work with XML. * @@ -36,38 +38,36 @@ private XMLUtil() { * @return The new created text. */ public static String replaceTags(String text, ITagReplacer replacer) { - if (text != null && replacer != null) { - StringBuilder sb = new StringBuilder(); - char[] signs = text.toCharArray(); - boolean inTag = false; - boolean inAttribute = false; - StringBuilder tagSB = null; - for (char sign : signs) { - if (!inTag) { - if (sign == '<') { - inTag = true; - tagSB = new StringBuilder(); - tagSB.append(sign); - } else { - sb.append(sign); - } - } else { + StringBuilder sb = new StringBuilder(); + char[] signs = text.toCharArray(); + boolean inTag = false; + boolean inAttribute = false; + StringBuilder tagSB = null; + for (char sign : signs) { + if (!inTag) { + if (sign == '<') { + inTag = true; + tagSB = new StringBuilder(); tagSB.append(sign); - if (sign == '>' && !inAttribute) { - inTag = false; - String replacement = replacer.replaceTag(tagSB.toString()); - if (replacement != null) { - sb.append(replacement); - } - } else if (sign == '\'' || sign == '"') { - inAttribute = !inAttribute; + } else { + sb.append(sign); + } + } else { + assert tagSB != null + : "@AssumeAssertion(nullness): tagSB must have been intialised already"; + tagSB.append(sign); + if (sign == '>' && !inAttribute) { + inTag = false; + String replacement = replacer.replaceTag(tagSB.toString()); + if (replacement != null) { + sb.append(replacement); } + } else if (sign == '\'' || sign == '"') { + inAttribute = !inAttribute; } } - return sb.toString(); - } else { - return null; } + return sb.toString(); } /** @@ -83,6 +83,7 @@ public interface ITagReplacer { * @param tag The found tag. * @return The replacement to use or {@code null} to remove the tag. */ + @Nullable String replaceTag(String tag); } @@ -95,7 +96,7 @@ public interface ITagReplacer { */ public static class HTMLRendererReplacer implements ITagReplacer { @Override - public String replaceTag(String tag) { + public @Nullable String replaceTag(String tag) { if (tag.startsWith("' && !inAttribute) { - inTag = false; - } else if (sign == '\'' || sign == '"') { - inAttribute = !inAttribute; - } + sb.append(sign); + } + } else { + if (sign == '>' && !inAttribute) { + inTag = false; + } else if (sign == '\'' || sign == '"') { + inAttribute = !inAttribute; } } - return sb.toString(); - } else { - return null; } + return sb.toString(); } /** @@ -170,23 +167,19 @@ public static String removeTags(String text) { * @return The encoded text. */ public static String encodeText(String text) { - if (text != null) { - char[] signs = text.toCharArray(); - StringBuilder sb = new StringBuilder(); - for (char sign : signs) { - switch (sign) { - case '"' -> sb.append("""); - case '&' -> sb.append("&"); - case '\'' -> sb.append("'"); - case '<' -> sb.append("<"); - case '>' -> sb.append(">"); - default -> sb.append(sign); - } + char[] signs = text.toCharArray(); + StringBuilder sb = new StringBuilder(); + for (char sign : signs) { + switch (sign) { + case '"' -> sb.append("""); + case '&' -> sb.append("&"); + case '\'' -> sb.append("'"); + case '<' -> sb.append("<"); + case '>' -> sb.append(">"); + default -> sb.append(sign); } - return sb.toString(); - } else { - return null; } + return sb.toString(); } /** diff --git a/key.util/src/main/java/org/key_project/util/java/package-info.java b/key.util/src/main/java/org/key_project/util/java/package-info.java new file mode 100644 index 00000000000..19d34270142 --- /dev/null +++ b/key.util/src/main/java/org/key_project/util/java/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (24.07.23) + */ +@NullMarked +package org.key_project.util.java; + +import org.jspecify.annotations.NullMarked; diff --git a/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithException.java b/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithException.java index 9fdae18a51d..52b8bea53d7 100644 --- a/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithException.java +++ b/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithException.java @@ -3,6 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.java.thread; +import org.checkerframework.checker.nullness.qual.MonotonicNonNull; +import org.jspecify.annotations.Nullable; + /** *

* Provides a basic implementation of {@link IRunnableWithException}. @@ -19,13 +22,13 @@ public abstract class AbstractRunnableWithException implements IRunnableWithExce /** * An occurred exception. */ - private Exception exception; + private @MonotonicNonNull Exception exception; /** * {@inheritDoc} */ @Override - public Exception getException() { + public @Nullable Exception getException() { return exception; } diff --git a/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithResult.java b/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithResult.java index 0af9a762996..baa8c020edc 100644 --- a/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithResult.java +++ b/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithResult.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.java.thread; +import org.jspecify.annotations.Nullable; + /** *

* Provides a basic implementation of {@link IRunnableWithResult}. @@ -20,13 +22,13 @@ public abstract class AbstractRunnableWithResult extends AbstractRunnableWith /** * The result. */ - private T result; + private @Nullable T result; /** * {@inheritDoc} */ @Override - public T getResult() { + public @Nullable T getResult() { return result; } @@ -35,7 +37,7 @@ public T getResult() { * * @param result The result to set. */ - protected void setResult(T result) { + protected void setResult(@Nullable T result) { this.result = result; } } diff --git a/key.util/src/main/java/org/key_project/util/java/thread/IRunnableWithException.java b/key.util/src/main/java/org/key_project/util/java/thread/IRunnableWithException.java index 917329688b1..91c60d95c60 100644 --- a/key.util/src/main/java/org/key_project/util/java/thread/IRunnableWithException.java +++ b/key.util/src/main/java/org/key_project/util/java/thread/IRunnableWithException.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.java.thread; +import org.jspecify.annotations.Nullable; + /** *

* A {@link Runnable} that provides access to an exception that occurred during execution @@ -21,5 +23,6 @@ public interface IRunnableWithException extends Runnable { * * @return An occurred exception. */ + @Nullable Exception getException(); } diff --git a/key.util/src/main/java/org/key_project/util/java/thread/IRunnableWithResult.java b/key.util/src/main/java/org/key_project/util/java/thread/IRunnableWithResult.java index 14311bdc90a..31ee5a9ce68 100644 --- a/key.util/src/main/java/org/key_project/util/java/thread/IRunnableWithResult.java +++ b/key.util/src/main/java/org/key_project/util/java/thread/IRunnableWithResult.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.java.thread; +import org.jspecify.annotations.Nullable; + /** *

* A {@link Runnable} that has a result that is accessible via {@link #getResult()}. @@ -20,6 +22,7 @@ public interface IRunnableWithResult extends IRunnableWithException { * * @return The result. */ + @Nullable T getResult(); /** @@ -27,5 +30,6 @@ public interface IRunnableWithResult extends IRunnableWithException { * * @return An occurred exception. */ + @Nullable Exception getException(); } diff --git a/key.util/src/main/java/org/key_project/util/java/thread/package-info.java b/key.util/src/main/java/org/key_project/util/java/thread/package-info.java new file mode 100644 index 00000000000..4b58f90e8e6 --- /dev/null +++ b/key.util/src/main/java/org/key_project/util/java/thread/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (24.07.23) + */ +@NullMarked +package org.key_project.util.java.thread; + +import org.jspecify.annotations.NullMarked; diff --git a/key.util/src/main/java/org/key_project/util/lookup/InjectionException.java b/key.util/src/main/java/org/key_project/util/lookup/InjectionException.java index 968a233c528..07b807c095e 100644 --- a/key.util/src/main/java/org/key_project/util/lookup/InjectionException.java +++ b/key.util/src/main/java/org/key_project/util/lookup/InjectionException.java @@ -7,6 +7,7 @@ * @author Alexander Weigl * @version 1 (13.01.19) */ +@SuppressWarnings("nullness") public class InjectionException extends RuntimeException { private static final long serialVersionUID = 119998955722036861L; diff --git a/key.util/src/main/java/org/key_project/util/lookup/Lookup.java b/key.util/src/main/java/org/key_project/util/lookup/Lookup.java index e8ab359ad24..a61dce2197a 100644 --- a/key.util/src/main/java/org/key_project/util/lookup/Lookup.java +++ b/key.util/src/main/java/org/key_project/util/lookup/Lookup.java @@ -9,6 +9,10 @@ import java.lang.reflect.Method; import java.util.*; +import org.checkerframework.checker.initialization.qual.Initialized; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + /** * This class handles the management of services and implementations. *

@@ -21,10 +25,11 @@ * @author Alexander Weigl * @version 1 (15.03.19) */ +@NullMarked public class Lookup { - public static Lookup DEFAULT = new Lookup(); + public static final Lookup DEFAULT = new Lookup(); - private final Lookup parent; + private final @Nullable Lookup parent; /** * Registered services. The first service in the list is the default. @@ -45,10 +50,13 @@ public Lookup() { this(null); } - public Lookup(Lookup parent) { + public Lookup(@Nullable Lookup parent) { this.parent = parent; if (parent != null) { - parent.children.add(new WeakReference<>(this)); + @SuppressWarnings("nullness") // WeakReference to this + @Initialized + WeakReference weakthis = new WeakReference<>(this); + parent.children.add(weakthis); } } @@ -83,7 +91,7 @@ public Collection lookupAll(Class service) { * @param * @return */ - public T get(Class service) { + public T get(Class service) { List t = getList(service); if (t.isEmpty()) { if (parent != null) { @@ -134,7 +142,7 @@ public void dispose() { } } - public List getListeners(Class name) { + public List getListeners(Class name) { return propertyListener.computeIfAbsent(name, a -> new LinkedList<>()); } @@ -142,11 +150,11 @@ public void addChangeListener(LookupListener listener) { addChangeListener(ALL.class, listener); } - public void addChangeListener(Class name, LookupListener listener) { + public void addChangeListener(Class name, LookupListener listener) { getListeners(name).add(listener); } - public void removeChangeListener(Class name, LookupListener listener) { + public void removeChangeListener(Class name, LookupListener listener) { getListeners(name).remove(listener); } @@ -178,7 +186,7 @@ public void register(T o) { } @SuppressWarnings("unchecked") - private List getList(Class service) { + private List getList(Class service) { return (List) serviceMap.computeIfAbsent(service, (k -> new LinkedList<>())); } @@ -191,8 +199,10 @@ private List getList(Class service) { * @return * @throws InjectionException if non suitable constructors could be found. */ - @SuppressWarnings("unchecked") - public T createInstance(Class clazz) throws InjectionException { + @SuppressWarnings({ "unchecked", + "keyfor", "nullness", // KeyFor and type variable bounds + }) + public @Nullable T createInstance(Class clazz) throws InjectionException { for (Constructor ctor : clazz.getConstructors()) { if (ctor.getAnnotation(Inject.class) != null) { T instance = (T) tryToInject(ctor); @@ -210,13 +220,15 @@ public T createInstance(Class clazz) throws InjectionException { * @return * @throws InjectionException */ - protected T tryToInject(Constructor ctor) throws InjectionException { + protected @Nullable T tryToInject(Constructor ctor) throws InjectionException { List services = Arrays.stream(ctor.getParameterTypes()).map(this::get).toList(); if (services.stream().allMatch(Objects::nonNull)) { try { - return ctor.newInstance(services.toArray()); + @SuppressWarnings("nullness") // connection to allMatch lost + T res = ctor.newInstance(services.toArray()); + return res; } catch (InstantiationException | IllegalAccessException | InvocationTargetException e) { throw new InjectionException(e); diff --git a/key.util/src/main/java/org/key_project/util/package-info.java b/key.util/src/main/java/org/key_project/util/package-info.java new file mode 100644 index 00000000000..5a4916969b6 --- /dev/null +++ b/key.util/src/main/java/org/key_project/util/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (24.07.23) + */ +@NullMarked +package org.key_project.util; + +import org.jspecify.annotations.NullMarked; diff --git a/key.util/src/main/java/org/key_project/util/reflection/package-info.java b/key.util/src/main/java/org/key_project/util/reflection/package-info.java new file mode 100644 index 00000000000..5c2695077d4 --- /dev/null +++ b/key.util/src/main/java/org/key_project/util/reflection/package-info.java @@ -0,0 +1,4 @@ +@NullMarked +package org.key_project.util.reflection; + +import org.jspecify.annotations.NullMarked; diff --git a/key.util/src/main/java/org/key_project/util/testcategories/Interactive.java b/key.util/src/main/java/org/key_project/util/testcategories/Interactive.java index fe5f22bab68..8b9b6272f9e 100644 --- a/key.util/src/main/java/org/key_project/util/testcategories/Interactive.java +++ b/key.util/src/main/java/org/key_project/util/testcategories/Interactive.java @@ -4,7 +4,7 @@ package org.key_project.util.testcategories; /** - * These test should never be executed by CIs, because they require manual interaction. + * CIs should never execute these tests, because they require manual interaction. */ public interface Interactive { } diff --git a/key.util/src/main/java/org/key_project/util/testcategories/Slow.java b/key.util/src/main/java/org/key_project/util/testcategories/Slow.java index c16316daced..31836735744 100644 --- a/key.util/src/main/java/org/key_project/util/testcategories/Slow.java +++ b/key.util/src/main/java/org/key_project/util/testcategories/Slow.java @@ -4,7 +4,7 @@ package org.key_project.util.testcategories; /** - * Category for slow test cases, that should only consider on Jenkins (merge request and master). + * Category for slow test cases, that should only consider on Jenkins (merge request and main). */ public interface Slow { } diff --git a/key.util/src/main/java/org/key_project/util/testcategories/package-info.java b/key.util/src/main/java/org/key_project/util/testcategories/package-info.java index a23e3782c42..31b3f4f9f6e 100644 --- a/key.util/src/main/java/org/key_project/util/testcategories/package-info.java +++ b/key.util/src/main/java/org/key_project/util/testcategories/package-info.java @@ -7,4 +7,7 @@ * @date 2019-04-18 * @see "https://dzone.com/articles/closer-look-junit-categories" */ +@NullMarked package org.key_project.util.testcategories; + +import org.jspecify.annotations.NullMarked; diff --git a/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java b/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java index 24ad263cdcd..e97c6d53814 100644 --- a/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java +++ b/key.util/src/test/java/org/key_project/util/collection/TestImmutables.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.collection; +import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.Test; import static org.junit.jupiter.api.Assertions.*; @@ -34,17 +35,20 @@ public void testRemoveDuplicatesLarge() { @Test public void testRemoveDuplicates() { + @Nullable String[][] a = { { "a", "b", "a", "c", "d", "d", "a", "e" }, { null, "a", null }, { "1", "1", "1", "1", "1" } }; + @Nullable String[][] expected = { { "a", "b", "c", "d", "e" }, { null, "a" }, { "1" } }; for (int i = 0; i < a.length; i++) { - ImmutableList l = ImmutableSLList.nil().prepend(a[i]).reverse(); + ImmutableList<@Nullable String> l = + ImmutableSLList.<@Nullable String>nil().prepend(a[i]).reverse(); assertFalse(Immutables.isDuplicateFree(l)); - ImmutableList cleaned = Immutables.removeDuplicates(l); + ImmutableList<@Nullable String> cleaned = Immutables.removeDuplicates(l); String[] a2 = cleaned.reverse().toArray(String.class); @@ -65,25 +69,31 @@ public void testRemoveDuplicatesIdentical() { @Test public void testIsDuplicateFree() { + @Nullable String[][] a = { { "a", "b", "c", "d", "e" }, {}, { "a" }, { null }, { null, "a" } }; - for (String[] strings : a) { - ImmutableList l = ImmutableSLList.nil().prepend(strings); + for (@Nullable + String[] strings : a) { + ImmutableList<@Nullable String> l = + ImmutableSLList.<@Nullable String>nil().prepend(strings); assertTrue(Immutables.isDuplicateFree(l)); } + @Nullable String[][] b = { { "a", "a" }, { "a", "b", "c", "d", "a" }, { "a", "b", "a", "d", "e" }, { "a", "b", "d", "d", "e" }, { "a", "b", "c", "d", "d" }, { null, "a", null } }; - for (String[] strings : b) { - ImmutableList l = ImmutableSLList.nil().prepend(strings); + for (@Nullable + String[] strings : b) { + ImmutableList<@Nullable String> l = + ImmutableSLList.<@Nullable String>nil().prepend(strings); assertFalse(Immutables.isDuplicateFree(l)); } } - private static void assertDeepEquals(Object[] expected, Object[] array) { + private static void assertDeepEquals(@Nullable Object[] expected, @Nullable Object[] array) { assertEquals(expected.length, array.length); for (int i = 0; i < array.length; i++) { assertEquals(expected[i], array[i]); diff --git a/key.util/src/test/java/org/key_project/util/model/ClassA.java b/key.util/src/test/java/org/key_project/util/model/ClassA.java index 25b2b28889e..97483d79cc0 100644 --- a/key.util/src/test/java/org/key_project/util/model/ClassA.java +++ b/key.util/src/test/java/org/key_project/util/model/ClassA.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.model; -@SuppressWarnings("unused") +@SuppressWarnings({ "unused", "nullness" }) public class ClassA { private final int privateField = 1; diff --git a/key.util/src/test/java/org/key_project/util/testcase/collection/TestLeftistHeapOfInteger.java b/key.util/src/test/java/org/key_project/util/testcase/collection/TestLeftistHeapOfInteger.java index 3058ad1c094..bb5a03f8942 100644 --- a/key.util/src/test/java/org/key_project/util/testcase/collection/TestLeftistHeapOfInteger.java +++ b/key.util/src/test/java/org/key_project/util/testcase/collection/TestLeftistHeapOfInteger.java @@ -19,6 +19,7 @@ import static org.junit.jupiter.api.Assertions.assertSame; import static org.junit.jupiter.api.Assertions.assertTrue; +@SuppressWarnings("initialization") public class TestLeftistHeapOfInteger { ImmutableList a; diff --git a/key.util/src/test/java/org/key_project/util/testcase/collection/TestMapAsListFromIntegerToString.java b/key.util/src/test/java/org/key_project/util/testcase/collection/TestMapAsListFromIntegerToString.java index 61c7f52c134..7d492d19e3a 100644 --- a/key.util/src/test/java/org/key_project/util/testcase/collection/TestMapAsListFromIntegerToString.java +++ b/key.util/src/test/java/org/key_project/util/testcase/collection/TestMapAsListFromIntegerToString.java @@ -14,8 +14,7 @@ /** * JUnit test for MapAsList implementation */ - - +@SuppressWarnings("initialization") public class TestMapAsListFromIntegerToString { private String[] entryStr; diff --git a/key.util/src/test/java/org/key_project/util/testcase/collection/TestSLListOfString.java b/key.util/src/test/java/org/key_project/util/testcase/collection/TestSLListOfString.java index 90af33bf6fe..e621abd3c76 100644 --- a/key.util/src/test/java/org/key_project/util/testcase/collection/TestSLListOfString.java +++ b/key.util/src/test/java/org/key_project/util/testcase/collection/TestSLListOfString.java @@ -9,6 +9,7 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; import org.slf4j.Logger; @@ -19,6 +20,7 @@ /** * tests non-destructive list implementation with String */ +@SuppressWarnings("initialization") public class TestSLListOfString { private static final Logger LOGGER = LoggerFactory.getLogger(TestSLListOfString.class); @@ -29,8 +31,8 @@ public class TestSLListOfString { ImmutableList b; // "A" "B" ImmutableList c; // "A" "B" "C" "D" ImmutableList d; // "A" "B" "A" - ImmutableList e; // "A" "B" null - ImmutableList e1; // "A" "B" null + ImmutableList<@Nullable String> e; // "A" "B" null + ImmutableList<@Nullable String> e1; // "A" "B" null @BeforeEach @@ -40,8 +42,10 @@ public void setUp() { b = ImmutableSLList.nil().prepend("B").prepend("A"); c = ImmutableSLList.nil().prepend("D").prepend("C").prepend("B").prepend("A"); d = ImmutableSLList.nil().prepend("A").prepend("B").prepend("A"); - e = ImmutableSLList.nil().prepend((String) null).prepend("B").prepend("A"); - e1 = ImmutableSLList.nil().prepend((String) null).prepend("B").prepend("A"); + e = ImmutableSLList.<@Nullable String>nil().prepend((String) null).prepend("B") + .prepend("A"); + e1 = ImmutableSLList.<@Nullable String>nil().prepend((String) null).prepend("B") + .prepend("A"); } // tests prepend and implicitly iterator, size diff --git a/key.util/src/test/java/org/key_project/util/testcase/java/ArrayUtilTest.java b/key.util/src/test/java/org/key_project/util/testcase/java/ArrayUtilTest.java index 6a80dd23658..d0122cb7ed5 100644 --- a/key.util/src/test/java/org/key_project/util/testcase/java/ArrayUtilTest.java +++ b/key.util/src/test/java/org/key_project/util/testcase/java/ArrayUtilTest.java @@ -8,6 +8,7 @@ import org.key_project.util.java.ArrayUtil; import org.key_project.util.java.StringUtil; +import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.Test; import static org.junit.jupiter.api.Assertions.*; @@ -20,24 +21,15 @@ public class ArrayUtilTest { @Test public void testInsert() { + @Nullable String[] array = { "A", "B", "C" }; // Test possible indices assertArray(ArrayUtil.insert(array, "X", 0), "X", "A", "B", "C"); assertArray(ArrayUtil.insert(array, "X", 1), "A", "X", "B", "C"); assertArray(ArrayUtil.insert(array, "X", 2), "A", "B", "X", "C"); assertArray(ArrayUtil.insert(array, "X", 3), "A", "B", "C", "X"); - // Test null array - assertArray(ArrayUtil.insert(null, "X", 0), "X"); // Test null element assertArray(ArrayUtil.insert(array, null, 1), "A", null, "B", "C"); - // Test null array an delement - try { - ArrayUtil.insert(null, null, 0); - fail(); - } catch (IllegalArgumentException e) { - assertEquals("Can not create an array if array and element to insert are null.", - e.getMessage()); - } // Test invalid indices try { ArrayUtil.insert(array, "X", -1); @@ -52,7 +44,7 @@ public void testInsert() { } @SuppressWarnings("unchecked") - private void assertArray(T[] current, T... expected) { + private void assertArray(T[] current, T... expected) { assertNotNull(current); assertEquals(current.length, expected.length); for (int i = 0; i < current.length; i++) { @@ -65,14 +57,13 @@ private void assertArray(T[] current, T... expected) { */ @Test public void testSearch() { + @Nullable String[] array = { "A", "B", "C", "D" }; - assertEquals("A", ArrayUtil.search(array, "A"::equals)); - assertEquals("B", ArrayUtil.search(array, "B"::equals)); - assertEquals("C", ArrayUtil.search(array, "C"::equals)); - assertEquals("D", ArrayUtil.search(array, "D"::equals)); - assertNull(ArrayUtil.search(array, "E"::equals)); - assertNull(ArrayUtil.search(array, null)); - assertNull(ArrayUtil.search(null, "E"::equals)); + assertEquals("A", ArrayUtil.<@Nullable String>search(array, "A"::equals)); + assertEquals("B", ArrayUtil.<@Nullable String>search(array, "B"::equals)); + assertEquals("C", ArrayUtil.<@Nullable String>search(array, "C"::equals)); + assertEquals("D", ArrayUtil.<@Nullable String>search(array, "D"::equals)); + assertNull(ArrayUtil.<@Nullable String>search(array, "E"::equals)); } /** @@ -80,7 +71,6 @@ public void testSearch() { */ @Test public void testIsEmpty() { - assertTrue(ArrayUtil.isEmpty(null)); assertTrue(ArrayUtil.isEmpty(new String[] {})); assertFalse(ArrayUtil.isEmpty(new String[] { "A" })); assertFalse(ArrayUtil.isEmpty(new String[] { null })); @@ -92,12 +82,10 @@ public void testIsEmpty() { */ @Test public void testToString_int_String() { - assertEquals(StringUtil.EMPTY_STRING, ArrayUtil.toString((int[]) null, ";")); assertEquals(StringUtil.EMPTY_STRING, ArrayUtil.toString(new int[] {}, ";")); assertEquals("1", ArrayUtil.toString(new int[] { 1 }, ";")); assertEquals("1;2", ArrayUtil.toString(new int[] { 1, 2 }, ";")); assertEquals("1;2;3", ArrayUtil.toString(new int[] { 1, 2, 3 }, ";")); - assertEquals("1null2null3", ArrayUtil.toString(new int[] { 1, 2, 3 }, null)); } /** @@ -105,7 +93,6 @@ public void testToString_int_String() { */ @Test public void testToString_int() { - assertEquals(StringUtil.EMPTY_STRING, ArrayUtil.toString((int[]) null)); assertEquals(StringUtil.EMPTY_STRING, ArrayUtil.toString(new int[] {})); assertEquals("1", ArrayUtil.toString(new int[] { 1 })); assertEquals("1, 2", ArrayUtil.toString(new int[] { 1, 2 })); @@ -117,14 +104,11 @@ public void testToString_int() { */ @Test public void testToString_Object_String() { - assertEquals(StringUtil.EMPTY_STRING, ArrayUtil.toString((String[]) null, ";")); assertEquals(StringUtil.EMPTY_STRING, ArrayUtil.toString(new String[] {}, ";")); assertEquals("A", ArrayUtil.toString(new String[] { "A" }, ";")); assertEquals("A;B", ArrayUtil.toString(new String[] { "A", "B" }, ";")); assertEquals("A;B;null", ArrayUtil.toString(new String[] { "A", "B", null }, ";")); assertEquals("A;B;null;D", ArrayUtil.toString(new String[] { "A", "B", null, "D" }, ";")); - assertEquals("AnullBnullnullnullD", - ArrayUtil.toString(new String[] { "A", "B", null, "D" }, null)); } /** @@ -132,7 +116,6 @@ public void testToString_Object_String() { */ @Test public void testToString_Object() { - assertEquals(StringUtil.EMPTY_STRING, ArrayUtil.toString((String[]) null)); assertEquals(StringUtil.EMPTY_STRING, ArrayUtil.toString(new String[] {})); assertEquals("A", ArrayUtil.toString(new String[] { "A" })); assertEquals("A, B", ArrayUtil.toString(new String[] { "A", "B" })); @@ -146,7 +129,8 @@ public void testToString_Object() { @Test public void testRemove() { // Test remove on array - String[] array = new String[] { "A", "B", "C", null, "D", null, null, "C", "A" }; + @Nullable + String[] array = new @Nullable String[] { "A", "B", "C", null, "D", null, null, "C", "A" }; array = ArrayUtil.remove(array, "B"); // Remove B assertArrayEquals(array, "A", "C", null, "D", null, null, "C", "A"); array = ArrayUtil.remove(array, "B"); // Remove B again @@ -163,9 +147,6 @@ public void testRemove() { assertArrayEquals(array); array = ArrayUtil.remove(array, "A"); // Remove A assertArrayEquals(array); - // Test null array - array = ArrayUtil.remove(null, "X"); - assertNull(array); } /** @@ -190,32 +171,14 @@ protected void assertArrayEquals(T[] array, T... expectedValues) { public void testAddAll() { String[] first = new String[] { "A", "B", "C" }; String[] second = new String[] { "D", "E" }; - // Test first parameter null - String[] combined = ArrayUtil.addAll(null, second); - assertEquals(2, combined.length); - assertEquals("D", combined[0]); - assertEquals("E", combined[1]); - // Test second parameter null - combined = ArrayUtil.addAll(first, null); - assertEquals(3, combined.length); - assertEquals("A", combined[0]); - assertEquals("B", combined[1]); - assertEquals("C", combined[2]); - // Test both parameter valid - combined = ArrayUtil.addAll(first, second); + @Nullable + String[] combined = ArrayUtil.addAll(first, second); assertEquals(5, combined.length); assertEquals("A", combined[0]); assertEquals("B", combined[1]); assertEquals("C", combined[2]); assertEquals("D", combined[3]); assertEquals("E", combined[4]); - // Test both parameter null - try { - ArrayUtil.addAll(null, null); - fail("Exception expected if both parameters are null."); - } catch (IllegalArgumentException e) { - assertEquals("Can not create an array if both paramters are null.", e.getMessage()); - } } /** @@ -225,21 +188,8 @@ public void testAddAll() { public void testAddAll_newType() { String[] first = new String[] { "A", "B", "C" }; String[] second = new String[] { "D", "E" }; - // Test first parameter null - Object[] combined = ArrayUtil.addAll(null, second, Object.class); - assertEquals(Object.class, combined.getClass().getComponentType()); - assertEquals(2, combined.length); - assertEquals("D", combined[0]); - assertEquals("E", combined[1]); - // Test second parameter null - combined = ArrayUtil.addAll(first, null, Object.class); - assertEquals(Object.class, combined.getClass().getComponentType()); - assertEquals(3, combined.length); - assertEquals("A", combined[0]); - assertEquals("B", combined[1]); - assertEquals("C", combined[2]); - // Test both parameter valid - combined = ArrayUtil.addAll(first, second, Object.class); + @Nullable + Object[] combined = ArrayUtil.addAll(first, second, Object.class); assertEquals(Object.class, combined.getClass().getComponentType()); assertEquals(5, combined.length); assertEquals("A", combined[0]); @@ -247,10 +197,6 @@ public void testAddAll_newType() { assertEquals("C", combined[2]); assertEquals("D", combined[3]); assertEquals("E", combined[4]); - // Test both parameter null - combined = ArrayUtil.addAll(null, null, Object.class); - assertEquals(Object.class, combined.getClass().getComponentType()); - assertEquals(0, combined.length); } /** @@ -258,14 +204,9 @@ public void testAddAll_newType() { */ @Test public void testAdd_int() { - // Test null array - int[] result = ArrayUtil.add(null, 1); - assertNotNull(result); - assertEquals(1, result.length); - assertEquals(1, result[0]); // Test empty array int[] array = new int[] {}; - result = ArrayUtil.add(array, 1); + int[] result = ArrayUtil.add(array, 1); assertNotNull(result); assertEquals(1, result.length); assertEquals(1, result[0]); @@ -300,14 +241,11 @@ public void testAdd_int() { */ @Test public void testAdd_Object() { - // Test null array - String[] result = ArrayUtil.add(null, "A"); - assertNotNull(result); - assertEquals(1, result.length); - assertEquals("A", result[0]); // Test empty array + @Nullable String[] array = new String[] {}; - result = ArrayUtil.add(array, "A"); + @Nullable + String[] result = ArrayUtil.add(array, "A"); assertNotNull(result); assertEquals(1, result.length); assertEquals("A", result[0]); @@ -344,13 +282,6 @@ public void testAdd_Object() { assertEquals("B", result[1]); assertEquals("C", result[2]); assertNull(result[3]); - // Test null new element on null array - try { - ArrayUtil.add(null, null); - fail("Exception expected if both parameters are null."); - } catch (IllegalArgumentException e) { - assertEquals("Can not create an array if both paramters are null.", e.getMessage()); - } } /** @@ -360,14 +291,13 @@ public void testAdd_Object() { public void testContains() { String[] array = { "A", "B", "C" }; assertFalse(ArrayUtil.contains(array, null)); - assertFalse(ArrayUtil.contains(null, "A")); assertTrue(ArrayUtil.contains(array, "A")); assertTrue(ArrayUtil.contains(array, "B")); assertTrue(ArrayUtil.contains(array, "C")); assertFalse(ArrayUtil.contains(array, "D")); + @Nullable String[] arrayWithNull = { "A", "B", null, "D" }; assertTrue(ArrayUtil.contains(arrayWithNull, null)); - assertFalse(ArrayUtil.contains(null, "A")); assertTrue(ArrayUtil.contains(arrayWithNull, "A")); assertTrue(ArrayUtil.contains(arrayWithNull, "B")); assertFalse(ArrayUtil.contains(arrayWithNull, "C")); @@ -375,7 +305,6 @@ public void testContains() { assertFalse(ArrayUtil.contains(arrayWithNull, "E")); String[] arrayWithDoubleElements = { "B", "A", "C", "B", "C" }; assertFalse(ArrayUtil.contains(arrayWithDoubleElements, null)); - assertFalse(ArrayUtil.contains(null, "A")); assertTrue(ArrayUtil.contains(arrayWithDoubleElements, "A")); assertTrue(ArrayUtil.contains(arrayWithDoubleElements, "B")); assertTrue(ArrayUtil.contains(arrayWithDoubleElements, "C")); @@ -389,14 +318,13 @@ public void testContains() { public void testIndexOf() { String[] array = { "A", "B", "C" }; assertEquals(-1, ArrayUtil.indexOf(array, null)); - assertEquals(-1, ArrayUtil.indexOf(null, "A")); assertEquals(0, ArrayUtil.indexOf(array, "A")); assertEquals(1, ArrayUtil.indexOf(array, "B")); assertEquals(2, ArrayUtil.indexOf(array, "C")); assertEquals(-1, ArrayUtil.indexOf(array, "D")); + @Nullable String[] arrayWithNull = { "A", "B", null, "D" }; assertEquals(2, ArrayUtil.indexOf(arrayWithNull, null)); - assertEquals(-1, ArrayUtil.indexOf(null, "A")); assertEquals(0, ArrayUtil.indexOf(arrayWithNull, "A")); assertEquals(1, ArrayUtil.indexOf(arrayWithNull, "B")); assertEquals(-1, ArrayUtil.indexOf(arrayWithNull, "C")); @@ -404,7 +332,6 @@ public void testIndexOf() { assertEquals(-1, ArrayUtil.indexOf(arrayWithNull, "E")); String[] arrayWithDoubleElements = { "B", "A", "C", "B", "C" }; assertEquals(-1, ArrayUtil.indexOf(arrayWithDoubleElements, null)); - assertEquals(-1, ArrayUtil.indexOf(null, "A")); assertEquals(1, ArrayUtil.indexOf(arrayWithDoubleElements, "A")); assertEquals(0, ArrayUtil.indexOf(arrayWithDoubleElements, "B")); assertEquals(2, ArrayUtil.indexOf(arrayWithDoubleElements, "C")); diff --git a/key.util/src/test/java/org/key_project/util/testcase/java/CollectionUtilTest.java b/key.util/src/test/java/org/key_project/util/testcase/java/CollectionUtilTest.java index a8e0c8dab81..c38f12143c1 100644 --- a/key.util/src/test/java/org/key_project/util/testcase/java/CollectionUtilTest.java +++ b/key.util/src/test/java/org/key_project/util/testcase/java/CollectionUtilTest.java @@ -9,6 +9,7 @@ import org.key_project.util.java.CollectionUtil; import org.key_project.util.java.IFilterWithException; +import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.Test; import static org.junit.jupiter.api.Assertions.*; @@ -37,11 +38,6 @@ public void testSearchAll() { // Test single not existing value found = CollectionUtil.searchAll(collection, "E"::equals); assertList(found); - // Test null - found = CollectionUtil.searchAll(collection, null); - assertList(found); - found = CollectionUtil.searchAll(null, "E"::equals); - assertList(found); // Test multible values found = CollectionUtil.searchAll(collection, element -> "A".equals(element) || "C".equals(element)); @@ -97,13 +93,11 @@ protected static void assertList(List actual, String... expected) { */ @Test public void testIndexOf_Iterator() { - List list = new LinkedList<>(); + List<@Nullable String> list = new LinkedList<>(); list.add("A"); list.add("B"); list.add("C"); - assertEquals(-1, CollectionUtil.indexOf((Iterator) null, null)); assertEquals(-1, CollectionUtil.indexOf(list.iterator(), null)); - assertEquals(-1, CollectionUtil.indexOf(null, "A")); assertEquals(0, CollectionUtil.indexOf(list.iterator(), "A")); assertEquals(1, CollectionUtil.indexOf(list.iterator(), "B")); assertEquals(2, CollectionUtil.indexOf(list.iterator(), "C")); @@ -153,9 +147,6 @@ public void testSearchAndRemoveWithException() throws Throwable { assertNull(CollectionUtil.searchAndRemoveWithException(collection, (IFilterWithException) "E"::equals)); assertEquals(collection, List.of()); - assertNull(CollectionUtil.searchAndRemoveWithException(collection, null)); - assertNull(CollectionUtil.searchAndRemoveWithException(null, - (IFilterWithException) "E"::equals)); assertEquals(collection, List.of()); } @@ -183,8 +174,6 @@ public void testSearchAndRemove() { assertEquals(collection, List.of()); assertNull(CollectionUtil.searchAndRemove(collection, "E"::equals)); assertEquals(collection, List.of()); - assertNull(CollectionUtil.searchAndRemove(collection, null)); - assertNull(CollectionUtil.searchAndRemove(null, "E"::equals)); assertEquals(collection, List.of()); } @@ -193,8 +182,6 @@ public void testSearchAndRemove() { */ @Test public void testRemoveFirst() { - // Test null - assertNull(CollectionUtil.removeFirst(null)); // Test empty collection Set set = new HashSet<>(); List list = new ArrayList<>(); @@ -223,28 +210,22 @@ public void testRemoveFirst() { @Test public void testContainsSame_List() { // Create model - List empty = new LinkedList<>(); - List one = Collections.singletonList("A"); - List oneCopy = Collections.singletonList("A"); - List oneDifferent = Collections.singletonList("B"); - List two = Arrays.asList("A", "B"); - List twoCopy = Arrays.asList("A", "B"); - List twoDifferent = Arrays.asList("C", "B"); - List twoChangedOrder = Arrays.asList("B", "A"); - List three = Arrays.asList("A", "B", "A"); - List threeCopy = Arrays.asList("A", "B", "A"); - List threeDifferent = Arrays.asList("A", "B", "B"); - List threeChangedOrder = Arrays.asList("A", "A", "B"); - List four = Arrays.asList("A", "B", null, "A"); - List fourCopy = Arrays.asList("A", "B", null, "A"); - List fourDifferent = Arrays.asList("A", null, null, "B"); - List fourChangedOrder = Arrays.asList(null, "A", "A", "B"); - // Test handlig of null - assertTrue(CollectionUtil.containsSame(null, null)); - assertTrue(CollectionUtil.containsSame(empty, null)); - assertTrue(CollectionUtil.containsSame(null, empty)); - assertFalse(CollectionUtil.containsSame(null, one)); - assertFalse(CollectionUtil.containsSame(one, null)); + List<@Nullable String> empty = new LinkedList<>(); + List<@Nullable String> one = Collections.singletonList("A"); + List<@Nullable String> oneCopy = Collections.singletonList("A"); + List<@Nullable String> oneDifferent = Collections.singletonList("B"); + List<@Nullable String> two = Arrays.asList("A", "B"); + List<@Nullable String> twoCopy = Arrays.asList("A", "B"); + List<@Nullable String> twoDifferent = Arrays.asList("C", "B"); + List<@Nullable String> twoChangedOrder = Arrays.asList("B", "A"); + List<@Nullable String> three = Arrays.asList("A", "B", "A"); + List<@Nullable String> threeCopy = Arrays.asList("A", "B", "A"); + List<@Nullable String> threeDifferent = Arrays.asList("A", "B", "B"); + List<@Nullable String> threeChangedOrder = Arrays.asList("A", "A", "B"); + List<@Nullable String> four = Arrays.asList("A", "B", null, "A"); + List<@Nullable String> fourCopy = Arrays.asList("A", "B", null, "A"); + List<@Nullable String> fourDifferent = Arrays.asList("A", null, null, "B"); + List<@Nullable String> fourChangedOrder = Arrays.asList(null, "A", "A", "B"); // Test one elements assertTrue(CollectionUtil.containsSame(one, one)); assertTrue(CollectionUtil.containsSame(one, oneCopy)); @@ -322,12 +303,6 @@ public void testContainsSame_Set() { Set twoCopy = Set.of("A", "B"); Set twoDifferent = Set.of("C", "B"); Set twoChangedOrder = Set.of("B", "A"); - // Test handlig of null - assertTrue(CollectionUtil.containsSame(null, null)); - assertTrue(CollectionUtil.containsSame(empty, null)); - assertTrue(CollectionUtil.containsSame(null, empty)); - assertFalse(CollectionUtil.containsSame(null, one)); - assertFalse(CollectionUtil.containsSame(one, null)); // Test one element assertTrue(CollectionUtil.containsSame(one, one)); assertTrue(CollectionUtil.containsSame(one, oneCopy)); @@ -360,9 +335,6 @@ public void testCount() { list.add("B"); list.add("A"); // Test counts - assertEquals(0, CollectionUtil.count(null, null)); - assertEquals(0, CollectionUtil.count(list, null)); - assertEquals(0, CollectionUtil.count(null, element -> false)); assertEquals(3, CollectionUtil.count(list, "A"::equals)); assertEquals(2, CollectionUtil.count(list, "B"::equals)); assertEquals(1, CollectionUtil.count(list, "C"::equals)); @@ -375,15 +347,13 @@ public void testCount() { @Test public void testContains() { // Create model - List list = new LinkedList<>(); + List<@Nullable String> list = new LinkedList<>(); list.add("A"); list.add("B"); list.add("C"); list.add("D"); // Test null parameter - assertFalse(CollectionUtil.contains(null, "A")); assertFalse(CollectionUtil.contains(list, null)); - assertFalse(CollectionUtil.contains(null, null)); // Test values assertTrue(CollectionUtil.contains(list, "A")); assertTrue(CollectionUtil.contains(list, "B")); @@ -406,8 +376,6 @@ public void testSearch() { assertEquals("C", CollectionUtil.search(collection, "C"::equals)); assertEquals("D", CollectionUtil.search(collection, "D"::equals)); assertNull(CollectionUtil.search(collection, "E"::equals)); - assertNull(CollectionUtil.search(collection, null)); - assertNull(CollectionUtil.search(null, "E"::equals)); } /** @@ -415,7 +383,7 @@ public void testSearch() { */ @Test public void testRemoveComplete() { - List collection = + List<@Nullable String> collection = new ArrayList<>(Arrays.asList("A", "B", "C", "A", "A", "B", "A", "D")); assertFalse(CollectionUtil.removeComplete(collection, null)); assertEquals("A", collection.get(0)); @@ -426,7 +394,6 @@ public void testRemoveComplete() { assertEquals("B", collection.get(5)); assertEquals("A", collection.get(6)); assertEquals("D", collection.get(7)); - assertFalse(CollectionUtil.removeComplete(null, "A")); assertEquals("A", collection.get(0)); assertEquals("B", collection.get(1)); assertEquals("C", collection.get(2)); @@ -468,9 +435,7 @@ public void testRemoveComplete() { @Test public void testAddAll_Iterable() { List collection = new LinkedList<>(); - CollectionUtil.addAll(null, List.of("A")); assertEquals(0, collection.size()); - CollectionUtil.addAll(collection, null); assertEquals(0, collection.size()); CollectionUtil.addAll(collection, List.of("A")); assertEquals(1, collection.size()); @@ -503,44 +468,11 @@ public void testAddAll_Iterable() { assertEquals("G", collection.get(6)); } - /** - * Test for {@link CollectionUtil#isEmpty(java.util.Collection)} - */ - @Test - public void testIsEmpty_Collection() { - assertTrue(CollectionUtil.isEmpty((Collection) null)); - List collection = new LinkedList<>(); - assertTrue(CollectionUtil.isEmpty(collection)); - collection.add("A"); - assertFalse(CollectionUtil.isEmpty(collection)); - collection.add("B"); - assertFalse(CollectionUtil.isEmpty(collection)); - collection.add("C"); - assertFalse(CollectionUtil.isEmpty(collection)); - } - - /** - * Test for {@link CollectionUtil#isEmpty(java.util.Map)} - */ - @Test - public void testIsEmpty_Map() { - assertTrue(CollectionUtil.isEmpty((Map) null)); - Map map = new HashMap<>(); - assertTrue(CollectionUtil.isEmpty(map)); - map.put("A", "A"); - assertFalse(CollectionUtil.isEmpty(map)); - map.put("B", "B"); - assertFalse(CollectionUtil.isEmpty(map)); - map.put("C", "C"); - assertFalse(CollectionUtil.isEmpty(map)); - } - /** * Test for {@link CollectionUtil#toString(java.util.Collection, String)} */ @Test public void testToString_Collection_String() { - assertEquals("", CollectionUtil.toString(null, " | ")); List collection = new LinkedList<>(); assertEquals("", CollectionUtil.toString(collection, " | ")); collection.add("A"); @@ -551,7 +483,6 @@ public void testToString_Collection_String() { assertEquals("A | B | C", CollectionUtil.toString(collection, " | ")); collection.add("D"); assertEquals("A | B | C | D", CollectionUtil.toString(collection, " | ")); - assertEquals("ABCD", CollectionUtil.toString(collection, null)); } /** @@ -559,7 +490,6 @@ public void testToString_Collection_String() { */ @Test public void testToString_Collection() { - assertEquals("", CollectionUtil.toString(null)); List collection = new LinkedList<>(); assertEquals("", CollectionUtil.toString(collection)); collection.add("A"); diff --git a/key.util/src/test/java/org/key_project/util/testcase/java/IOUtilTest.java b/key.util/src/test/java/org/key_project/util/testcase/java/IOUtilTest.java index 94f6b51b29e..920fa516e97 100644 --- a/key.util/src/test/java/org/key_project/util/testcase/java/IOUtilTest.java +++ b/key.util/src/test/java/org/key_project/util/testcase/java/IOUtilTest.java @@ -20,6 +20,7 @@ import org.key_project.util.java.IOUtil.LineInformation; import org.key_project.util.java.XMLUtil; +import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.Test; import org.xml.sax.Attributes; import org.xml.sax.SAXException; @@ -42,22 +43,6 @@ public void testGetCurrentDirectory() { assertNotNull(currentDir); } - /** - * Tests {@link IOUtil#exists(File)} - */ - @Test - public void testExists() throws IOException { - assertFalse(IOUtil.exists(null)); - File tempFile = File.createTempFile("IOUtilTest_", ".testExists"); - assertTrue(IOUtil.exists(tempFile)); - tempFile.delete(); - assertFalse(IOUtil.exists(tempFile)); - File tempDir = IOUtil.createTempDirectory("IOUtilTest_", ".testExists"); - assertTrue(IOUtil.exists(tempDir)); - IOUtil.delete(tempDir); - assertFalse(IOUtil.exists(tempDir)); - } - /** * {@link IOUtil#contains(Iterable, File)}. */ @@ -84,10 +69,10 @@ public void testContains_Iterable() throws IOException { File noSubFile = HelperClassForUtilityTests.createFile(new File(noFolder, "Hello.txt"), "Hello"); List parents = Arrays.asList(yesDir, alsoYesDir); - assertFalse(IOUtil.contains((Iterable) null, yesFile)); - assertFalse(IOUtil.contains(parents, null)); - assertFalse(IOUtil.contains((Iterable) null, null)); - assertFalse(IOUtil.contains(parents, yesDir.getParentFile())); + File yesDirParent = yesDir.getParentFile(); + if (yesDirParent != null) { + assertFalse(IOUtil.contains(yesDir, yesDirParent)); + } assertTrue(IOUtil.contains(parents, yesDir)); assertTrue(IOUtil.contains(parents, yesFile)); assertTrue(IOUtil.contains(parents, yesFolder)); @@ -125,10 +110,10 @@ public void testContains_File() throws IOException { File noFolder = HelperClassForUtilityTests.createFolder(new File(noDir, "yesSub")); File noSubFile = HelperClassForUtilityTests.createFile(new File(noFolder, "Hello.txt"), "Hello"); - assertFalse(IOUtil.contains((File) null, yesFile)); - assertFalse(IOUtil.contains(yesDir, null)); - assertFalse(IOUtil.contains((File) null, null)); - assertFalse(IOUtil.contains(yesDir, yesDir.getParentFile())); + File yesDirParent = yesDir.getParentFile(); + if (yesDirParent != null) { + assertFalse(IOUtil.contains(yesDir, yesDirParent)); + } assertTrue(IOUtil.contains(yesDir, yesDir)); assertTrue(IOUtil.contains(yesDir, yesFile)); assertTrue(IOUtil.contains(yesDir, yesFolder)); @@ -148,7 +133,6 @@ public void testContains_File() throws IOException { */ @Test public void testUnifyLineBreaks() throws IOException { - doTestUnifyLineBreaks(null, null); doTestUnifyLineBreaks("A\nB\rC\n\nD\r\rE", "A\nB\nC\n\nD\n\nE"); doTestUnifyLineBreaks("A\r\nE", "A\nE"); } @@ -161,9 +145,7 @@ public void testUnifyLineBreaks() throws IOException { * @throws IOException Occurred Exception. */ protected void doTestUnifyLineBreaks(String toTest, String expected) throws IOException { - ByteArrayInputStream in = - toTest != null ? new ByteArrayInputStream(toTest.getBytes(StandardCharsets.UTF_8)) - : null; + ByteArrayInputStream in = new ByteArrayInputStream(toTest.getBytes(StandardCharsets.UTF_8)); InputStream converted = IOUtil.unifyLineBreaks(in); assertEquals(expected, IOUtil.readFrom(converted)); } @@ -231,9 +213,6 @@ public void testVisit() throws IOException { IOUtil.writeTo(new FileOutputStream(text), "Text.txt"); // Create visitor LogVisitor visitor = new LogVisitor(); - // Test null - IOUtil.visit(null, visitor); - assertEquals(0, visitor.getVisitedFiles().size()); // Test visiting IOUtil.visit(tempDir, visitor); // Ensure same order in all operating systems @@ -305,24 +284,8 @@ public void testSearch() throws IOException { IOUtil.writeTo(new FileOutputStream(text), "Text.txt"); // Create filter Predicate filter = element -> element.getName().contains("Sub"); - // Test null - List result = IOUtil.search(null, filter); - assertEquals(0, result.size()); - // Test no filter - result = IOUtil.search(tempDir, null); - result.sort(Comparator.comparing(File::getAbsolutePath)); // Ensure same order in all - // operating systems - assertEquals(8, result.size()); - assertEquals(tempDir, result.get(0)); - assertEquals(text, result.get(1)); - assertEquals(emptyFolder, result.get(2)); - assertEquals(subDir, result.get(3)); - assertEquals(subFile, result.get(4)); - assertEquals(subSubDir, result.get(5)); - assertEquals(subSubA, result.get(6)); - assertEquals(subSubB, result.get(7)); // Test with filter - result = IOUtil.search(tempDir, filter); + List result = IOUtil.search(tempDir, filter); result.sort(Comparator.comparing(File::getAbsolutePath)); // Ensure same order in all // operating systems assertEquals(4, result.size()); @@ -340,7 +303,6 @@ public void testSearch() throws IOException { */ @Test public void testGetFileExtension() { - assertNull(IOUtil.getFileExtension(null)); assertNull(IOUtil.getFileExtension(new File(""))); assertNull(IOUtil.getFileExtension(new File("hello"))); assertNull(IOUtil.getFileExtension(new File("path", "hello"))); @@ -369,7 +331,6 @@ public void testGetHomeDirectory() { */ @Test public void testGetFileNameWithoutExtension() { - assertNull(IOUtil.getFileNameWithoutExtension(null)); assertEquals("test", IOUtil.getFileNameWithoutExtension("test.txt")); assertEquals("hello.world", IOUtil.getFileNameWithoutExtension("hello.world.diagram")); assertEquals("", IOUtil.getFileNameWithoutExtension(".project")); @@ -391,7 +352,9 @@ public void testCreateTempDirectory() throws IOException { assertTrue(tempDir.getName().startsWith("IOUtilTest")); assertTrue(tempDir.getName().endsWith("testCreateTempDirectory")); } finally { - IOUtil.delete(tempDir); + if (tempDir != null) { + IOUtil.delete(tempDir); + } } } @@ -461,8 +424,6 @@ public void testComputeLineInformation_File() throws IOException { File textFile = new File(HelperClassForUtilityTests.RESOURCE_DIRECTORY + File.separator + "lineIndicesTest" + File.separator + "Text.txt"); assertTrue(textFile.isFile(), "File '" + textFile + "' does not exist."); - // Test null - assertLineInformation((File) null); // Test unix file assertLineInformation(convertTextFile(textFile, "Text_Unix.txt", "\r"), 0, 1, 2, 9, 16, 17, 24, 50, 23661, 23662, 23663, 23671, 23672); @@ -550,8 +511,8 @@ public void testComputeLineInformation_InputStream() throws IOException { * @throws IOException Occurred Exception. */ protected void doTestComputeLineInformation_InputStream(String newLine) throws IOException { - // Test null - assertLineInformation(newLine, new String[0]); + // Test empty string + assertLineInformation(newLine, ""); // Test single line assertLineInformation(newLine, "Hello World!"); // Test two line @@ -591,32 +552,28 @@ protected void doTestComputeLineInformation_InputStream(String newLine) throws I * @throws IOException Occurred Exception. */ protected void assertLineInformation(String newLine, String... textLines) throws IOException { - if (textLines != null) { - StringBuilder sb = new StringBuilder(); - LineInformation[] expectedInfos = new LineInformation[textLines.length]; - int lastIndex = 0; - for (int i = 0; i < textLines.length; i++) { - // Compute tabs - List tabIndices = new LinkedList<>(); - char[] lineChars = textLines[i].toCharArray(); - for (int j = 0; j < lineChars.length; j++) { - if ('\t' == lineChars[j]) { - tabIndices.add(j); - } - } - // Compute line - expectedInfos[i] = new LineInformation(lastIndex, tabIndices); - sb.append(textLines[i]); - lastIndex += textLines[i].length(); - if (i < textLines.length - 1) { - sb.append(newLine); - lastIndex += newLine.length(); + StringBuilder sb = new StringBuilder(); + LineInformation[] expectedInfos = new LineInformation[textLines.length]; + int lastIndex = 0; + for (int i = 0; i < textLines.length; i++) { + // Compute tabs + List tabIndices = new LinkedList<>(); + char[] lineChars = textLines[i].toCharArray(); + for (int j = 0; j < lineChars.length; j++) { + if ('\t' == lineChars[j]) { + tabIndices.add(j); } } - assertLineInformation(sb.length() >= 1 ? sb.toString() : null, expectedInfos); - } else { - assertLineInformation(null, new LineInformation[0]); + // Compute line + expectedInfos[i] = new LineInformation(lastIndex, tabIndices); + sb.append(textLines[i]); + lastIndex += textLines[i].length(); + if (i < textLines.length - 1) { + sb.append(newLine); + lastIndex += newLine.length(); + } } + assertLineInformation(sb.toString(), expectedInfos); } /** @@ -629,7 +586,7 @@ protected void assertLineInformation(String newLine, String... textLines) throws protected void assertLineInformation(String text, LineInformation... expectedInfos) throws IOException { LineInformation[] result = IOUtil.computeLineInformation( - text != null ? new ByteArrayInputStream(text.getBytes(StandardCharsets.UTF_8)) : null); + new ByteArrayInputStream(text.getBytes(StandardCharsets.UTF_8))); assertNotNull(result, text); assertEquals(expectedInfos.length, result.length, text); for (int i = 0; i < expectedInfos.length; i++) { @@ -652,13 +609,8 @@ protected void assertLineInformation(String text, LineInformation... expectedInf public void testWriteTo() throws IOException { File tempFile = null; try { - // Test null stream, nothing should happen String content = "Hello World!"; - IOUtil.writeTo(null, content); - // Test null content ByteArrayOutputStream out = new ByteArrayOutputStream(); - IOUtil.writeTo(out, null); - assertEquals(0, out.toByteArray().length); // Test writing to memory stream out = new ByteArrayOutputStream(); IOUtil.writeTo(out, content); @@ -697,7 +649,7 @@ public void testWriteTo_Charstet() throws Exception { protected byte[] doWriteCharsetAsXmlTest(String text, Charset encoding) throws Exception { // Create XML StringBuilder sb = new StringBuilder(); - XMLUtil.appendXmlHeader(encoding != null ? encoding.displayName() : null, sb); + XMLUtil.appendXmlHeader(encoding.displayName(), sb); Map attributes = new LinkedHashMap<>(); attributes.put("text", XMLUtil.encodeText(text)); XMLUtil.appendEmptyTag(0, "root", attributes, sb); @@ -724,7 +676,7 @@ private static final class RootHandler extends DefaultHandler { /** * The parsed text. */ - private String text; + private @Nullable String text; /** * {@inheritDoc} @@ -748,7 +700,7 @@ public void startElement(String uri, String localName, String qName, Attributes * * @return The parsed text. */ - public String getText() { + public @Nullable String getText() { return text; } } @@ -758,8 +710,6 @@ public String getText() { */ @Test public void testReadFrom_File() throws IOException { - // Test null - assertNull(IOUtil.readFrom((File) null)); File tempFile = File.createTempFile("IOUtilTest", "testReadFrom_File"); try { // Test not existing file @@ -780,7 +730,6 @@ public void testReadFrom_File() throws IOException { @Test public void testReadFrom_InputStream() { try { - doTestReadFrom(null); doTestReadFrom("One Line"); doTestReadFrom("First Line\n\rSecond Line"); doTestReadFrom("One Line\r"); @@ -794,12 +743,8 @@ public void testReadFrom_InputStream() { } protected void doTestReadFrom(String text) throws IOException { - if (text != null) { - assertEquals(text, - IOUtil.readFrom(new ByteArrayInputStream(text.getBytes(StandardCharsets.UTF_8)))); - } else { - assertNull(IOUtil.readFrom((InputStream) null)); - } + assertEquals(text, + IOUtil.readFrom(new ByteArrayInputStream(text.getBytes(StandardCharsets.UTF_8)))); } /** @@ -807,8 +752,6 @@ protected void doTestReadFrom(String text) throws IOException { */ @Test public void testDelete() throws IOException { - // Test null - IOUtil.delete(null); // No exception expected // Test existing file File tmpFile = File.createTempFile("IOUtilTest", "deleteMe"); assertTrue(tmpFile.exists()); @@ -844,10 +787,6 @@ public void testDelete() throws IOException { */ @Test public void testCopy() throws IOException { - doTestCopy(null); - assertFalse(IOUtil.copy((InputStream) null, null)); - assertFalse(IOUtil.copy( - new ByteArrayInputStream("NotCopied".getBytes(StandardCharsets.UTF_8)), null)); doTestCopy("One Line"); doTestCopy("First Line\n\rSecond Line"); doTestCopy("One Line\r"); @@ -864,18 +803,14 @@ public void testCopy() throws IOException { * @throws IOException Occurred Exception. */ protected void doTestCopy(String text) throws IOException { - if (text != null) { - byte[] inBytes = text.getBytes(StandardCharsets.UTF_8); - ByteArrayInputStream in = new ByteArrayInputStream(inBytes); - ByteArrayOutputStream out = new ByteArrayOutputStream(); - assertTrue(IOUtil.copy(in, out)); - byte[] outBytes = out.toByteArray(); - assertEquals(inBytes.length, outBytes.length); - for (int i = 0; i < inBytes.length; i++) { - assertEquals(inBytes[i], outBytes[i]); - } - } else { - assertFalse(IOUtil.copy(null, new ByteArrayOutputStream())); + byte[] inBytes = text.getBytes(StandardCharsets.UTF_8); + ByteArrayInputStream in = new ByteArrayInputStream(inBytes); + ByteArrayOutputStream out = new ByteArrayOutputStream(); + assertTrue(IOUtil.copy(in, out)); + byte[] outBytes = out.toByteArray(); + assertEquals(inBytes.length, outBytes.length); + for (int i = 0; i < inBytes.length; i++) { + assertEquals(inBytes[i], outBytes[i]); } } @@ -884,7 +819,6 @@ protected void doTestCopy(String text) throws IOException { */ @Test public void testGetClassLocation() { - assertNull(IOUtil.getClassLocation(null)); assertNotNull(IOUtil.getClassLocation(getClass())); } @@ -893,7 +827,6 @@ public void testGetClassLocation() { */ @Test public void testGetProjectRoot() { - assertNull(IOUtil.getProjectRoot(null)); assertNotNull(IOUtil.getProjectRoot(getClass())); } @@ -969,7 +902,6 @@ public void testToFileString() throws MalformedURLException { */ @Test public void testValidateOSIndependentFileName() { - assertNull(IOUtil.validateOSIndependentFileName(null)); assertEquals("Hello_World", IOUtil.validateOSIndependentFileName("Hello World")); assertEquals("Hello_World_txt", IOUtil.validateOSIndependentFileName("Hello World.txt")); assertEquals("Hello__World_txt", IOUtil.validateOSIndependentFileName("Hello<>World.txt")); diff --git a/key.util/src/test/java/org/key_project/util/testcase/java/NumberUtilTest.java b/key.util/src/test/java/org/key_project/util/testcase/java/NumberUtilTest.java index 84c0be704fe..e5fbdba9bc2 100644 --- a/key.util/src/test/java/org/key_project/util/testcase/java/NumberUtilTest.java +++ b/key.util/src/test/java/org/key_project/util/testcase/java/NumberUtilTest.java @@ -8,7 +8,6 @@ import org.junit.jupiter.api.Test; import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.fail; /** * Tests for {@link NumberUtil}. @@ -32,12 +31,6 @@ public void testParseFullInt() { assertEquals(123, NumberUtil.parseFullInt(NumberUtil.toFullString(123))); assertEquals(Integer.MAX_VALUE, NumberUtil.parseFullInt(NumberUtil.toFullString(Integer.MAX_VALUE))); - try { - NumberUtil.parseFullInt(null); - fail(); - } catch (NumberFormatException e) { - assertEquals("Text not defined.", e.getMessage()); - } } /** @@ -56,12 +49,6 @@ public void testParseFullLong() { assertEquals(123, NumberUtil.parseFullLong(NumberUtil.toFullString(123))); assertEquals(Long.MAX_VALUE, NumberUtil.parseFullLong(NumberUtil.toFullString(Long.MAX_VALUE))); - try { - NumberUtil.parseFullInt(null); - fail(); - } catch (NumberFormatException e) { - assertEquals("Text not defined.", e.getMessage()); - } } /** diff --git a/key.util/src/test/java/org/key_project/util/testcase/java/StringUtilTest.java b/key.util/src/test/java/org/key_project/util/testcase/java/StringUtilTest.java index 9294b92aa93..6e165ac6aa6 100644 --- a/key.util/src/test/java/org/key_project/util/testcase/java/StringUtilTest.java +++ b/key.util/src/test/java/org/key_project/util/testcase/java/StringUtilTest.java @@ -7,6 +7,7 @@ import org.key_project.util.java.StringUtil; +import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.Test; import static org.junit.jupiter.api.Assertions.*; @@ -163,7 +164,6 @@ public void testToSingleLinedString() { public void testReplaceAll() { String text = "ABCDABCDABCDABCD"; assertNull(StringUtil.replaceAll(null, new char[] {}, 'X')); - assertEquals(text, StringUtil.replaceAll(text, null, 'X')); assertEquals(text, StringUtil.replaceAll(text, new char[] {}, 'X')); assertEquals("XBCDXBCDXBCDXBCD", StringUtil.replaceAll(text, new char[] { 'A' }, 'X')); assertEquals("AXCDAXCDAXCDAXCD", StringUtil.replaceAll(text, new char[] { 'B' }, 'X')); @@ -209,13 +209,6 @@ public void testRepeat() { assertEquals("#####", StringUtil.repeat("#", 5)); // Test line with multiple characters assertEquals("ABABAB", StringUtil.repeat("AB", 3)); - - // Test null text - try { - assertEquals("nullnullnullnull", StringUtil.repeat(null, 4)); - fail(); - } catch (NullPointerException expected) { - } } /** @@ -223,7 +216,7 @@ public void testRepeat() { */ @Test public void testCreateIgnoreCaseComparator() { - Comparator c = StringUtil.createIgnoreCaseComparator(); + Comparator<@Nullable String> c = StringUtil.createIgnoreCaseComparator(); assertNotNull(c); assertSame("A".compareToIgnoreCase("A"), c.compare("A", "A")); assertSame("A".compareToIgnoreCase("a"), c.compare("A", "a")); diff --git a/key.util/src/test/java/org/key_project/util/testcase/java/XMLUtilTest.java b/key.util/src/test/java/org/key_project/util/testcase/java/XMLUtilTest.java index 281cfbbb497..d2ef7105106 100644 --- a/key.util/src/test/java/org/key_project/util/testcase/java/XMLUtilTest.java +++ b/key.util/src/test/java/org/key_project/util/testcase/java/XMLUtilTest.java @@ -13,7 +13,6 @@ import org.junit.jupiter.api.Test; import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertNull; /** * Tests for {@link XMLUtil}. @@ -26,15 +25,9 @@ public class XMLUtilTest { */ @Test public void testReplaceTags() { - assertNull(XMLUtil.replaceTags(null, null)); - assertNull(XMLUtil.replaceTags("Hello", null)); - assertNull(XMLUtil.replaceTags(null, new LoggingReplacer("|"))); assertReplaceTags("Hello World", "Hello World", "|"); assertReplaceTags("Hello
World", "|Hello| World|", "|", "", "
", ""); - assertReplaceTags("Hello World", "Hello World", null); - assertReplaceTags("Hello
World", "Hello World", null, "", "
", - ""); assertReplaceTags("Hello
World", "|Hello| World", "|", "", "
"); assertReplaceTags("Hello
World", "Hello| World|", "|", "
", ""); assertReplaceTags("Hello World", "|Hello World|", "|", @@ -49,7 +42,7 @@ public void testReplaceTags() { * @param text The text to execute * {@link XMLUtil#replaceTags(String, org.key_project.util.java.XMLUtil.ITagReplacer)} * on. - * @param expectedResult The expected result. + * @param expectedResult The expected result.N * @param fixedReplacement The fixed replacement to use. * @param expectedTags The expected found tags. */ @@ -115,7 +108,6 @@ public List getLog() { */ @Test public void testRemoveTags() { - assertNull(XMLUtil.removeTags(null)); assertEquals("Hello World", XMLUtil.removeTags("Hello World")); assertEquals("Hello World", XMLUtil.removeTags("Hello
World")); assertEquals("Hello World", XMLUtil.removeTags("Hello
World")); @@ -130,8 +122,6 @@ public void testRemoveTags() { */ @Test public void testEncodeText() { - // Test null - assertNull(XMLUtil.encodeText(null)); // Test empty string assertEquals(StringUtil.EMPTY_STRING, XMLUtil.encodeText(StringUtil.EMPTY_STRING)); // Text XML tags diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/actions/AddFormulaToSuccedentAction.java b/keyext.exploration/src/main/java/org/key_project/exploration/actions/AddFormulaToSuccedentAction.java index c4acd7fc56e..9c82697f90d 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/actions/AddFormulaToSuccedentAction.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/actions/AddFormulaToSuccedentAction.java @@ -13,7 +13,6 @@ import org.jspecify.annotations.NonNull; - /** * @author Alexander Weigl * @author Sarah Grebing diff --git a/settings.gradle b/settings.gradle index 65ec0e06535..171f3b1d56c 100644 --- a/settings.gradle +++ b/settings.gradle @@ -15,3 +15,7 @@ include 'keyext.proofmanagement' include 'keyext.exploration' include 'keyext.slicing' include 'keyext.caching' + +// ENABLE NULLNESS here or on the CLI +// This flag is activated to enable the checker framework. +// System.setProperty("ENABLE_NULLNESS", "true") \ No newline at end of file