diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index 48c0a02ca41..d6e308a6378 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.12-bin.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java index 18fe6e1daf1..e486b570b02 100644 --- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java @@ -96,7 +96,7 @@ public Proof getSource() { * {@inheritDoc} */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof IProofReference other) { return Objects.equals(getKind(), other.getKind()) && Objects.equals(getSource(), other.getSource()) diff --git a/key.core.rifl/build.gradle b/key.core.rifl/build.gradle index 393cf9f5cd4..31b34e40d4b 100644 --- a/key.core.rifl/build.gradle +++ b/key.core.rifl/build.gradle @@ -1,4 +1,20 @@ description "Support for the RS3 Information Flow Language (RIFL)" dependencies { implementation project (":key.core") -} \ No newline at end of file +} + +checkerFramework { + if(System.getProperty("ENABLE_NULLNESS")) { + checkers = [ + "org.checkerframework.checker.nullness.NullnessChecker", + ] + extraJavacArgs = [ + //"-AonlyDefs=^org\\.key_project\\.logic", + "-Xmaxerrs", "10000", + "-Astubs=$rootDir/key.util/src/main/checkerframework${File.pathSeparatorChar}permit-nullness-assertion-exception.astub", + "-AstubNoWarnIfNotFound", + "-Werror", + "-Aversion", + ] + } +} diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/DefaultSpecificationContainer.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/DefaultSpecificationContainer.java index 6363232a3ed..e64592b6c37 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/DefaultSpecificationContainer.java +++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/DefaultSpecificationContainer.java @@ -3,11 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.util.rifl; -import java.util.HashMap; -import java.util.LinkedHashSet; -import java.util.Map; +import java.util.*; import java.util.Map.Entry; -import java.util.Set; import de.uka.ilkd.key.util.rifl.SpecificationEntity.Field; import de.uka.ilkd.key.util.rifl.SpecificationEntity.Parameter; @@ -69,7 +66,8 @@ public String field(recoder.java.declaration.FieldDeclaration fd, Type type) { @Override public String field(String inPackage, String inClass, String name, Type type) { - return field2domain.get(new Field(name, inPackage, inClass, type)); + return Objects.requireNonNull(field2domain.get(new Field(name, inPackage, inClass, type)), + "Could not find field"); } @Override @@ -83,8 +81,10 @@ public String parameter(recoder.java.declaration.MethodDeclaration md, int index @Override public String parameter(String inPackage, String inClass, String methodName, String[] paramTypes, int index, Type type) { - return param2domain - .get(new Parameter(index, methodName, paramTypes, inPackage, inClass, type)); + return Objects.requireNonNull( + param2domain + .get(new Parameter(index, methodName, paramTypes, inPackage, inClass, type)), + "Parameter not found"); } @Override @@ -97,7 +97,9 @@ public String returnValue(recoder.java.declaration.MethodDeclaration md, Type ty @Override public String returnValue(String inPackage, String inClass, String methodName, String[] paramTypes, Type type) { - return return2domain.get(new ReturnValue(methodName, paramTypes, inPackage, inClass, type)); + return Objects.requireNonNull( + return2domain.get(new ReturnValue(methodName, paramTypes, inPackage, inClass, type)), + "Return value not found"); } @Override diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java index d8435fc1005..9fad14c19ca 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java +++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java @@ -8,9 +8,13 @@ import de.uka.ilkd.key.util.LinkedHashMap; +import org.checkerframework.checker.nullness.qual.EnsuresNonNull; +import org.checkerframework.checker.nullness.qual.KeyFor; +import org.checkerframework.checker.nullness.qual.MonotonicNonNull; import org.key_project.util.collection.KeYCollections; import org.key_project.util.collection.Pair; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; import org.xml.sax.Attributes; @@ -84,10 +88,10 @@ private static String printAttributes(Attributes a) { private final Map handles2categories = new LinkedHashMap<>(); private Set domains = new LinkedHashSet<>(); private Set> flow = new LinkedHashSet<>(); - private Map> tmpMap = null; - private Type type = null; + private Map> tmpMap = new HashMap<>(); + private Type type = Type.SOURCE; - private String tmpHandle = null; + private @MonotonicNonNull String tmpHandle = null; private String category = DEFAULT_CATEGORY; @@ -96,17 +100,20 @@ public RIFLHandler() { } private void assignHandle(Attributes attributes) { - final String handle = attributes.getValue("handle").intern(); + @SuppressWarnings("keyfor") + final @KeyFor("handles2categories") String handle = attributes.getValue("handle").intern(); final String domain = attributes.getValue("domain").intern(); Pair p = new Pair<>(handle, handles2categories.get(handle)); categories2domains.put(p, domain); } + @EnsuresNonNull("tmpHandle") private void setModifiable(Attributes attributes) { assert tmpHandle == null; tmpHandle = attributes.getValue("handle"); } + @SuppressWarnings("nullness") // uninitialization private void unsetModifiable() { assert tmpHandle != null; tmpHandle = null; @@ -125,7 +132,10 @@ public SpecificationContainer getSpecification() { return new DefaultSpecificationContainer(tmp, flow); } - private void putField(Attributes attributes) { + private void putField(Attributes attributes) throws SAXException { + if (tmpHandle == null) { + throw new SAXException("This element must be in a modifiable element!"); + } final String field = attributes.getValue("name"); final String clazz = attributes.getValue("class"); final String packg = attributes.getValue("package"); @@ -134,7 +144,10 @@ private void putField(Attributes attributes) { tmpMap.put(se, new Pair<>(tmpHandle, category)); } - private void putParam(Attributes attributes) { + private void putParam(Attributes attributes) throws SAXException { + if (tmpHandle == null) { + throw new SAXException("This element must be in a modifiable element!"); + } final String packg = attributes.getValue("package"); final String clazz = attributes.getValue("class"); final String method = attributes.getValue("method"); @@ -144,13 +157,16 @@ private void putParam(Attributes attributes) { tmpMap.put(se, new Pair<>(tmpHandle, category)); } - private void putReturn(Attributes attributes) { + private void putReturn(Attributes attributes) throws SAXException { + if (tmpHandle == null) { + throw new SAXException("This element must be in a modifiable element!"); + } final String packageName = attributes.getValue("package"); final String className = attributes.getValue("class"); final String methodName = attributes.getValue("method"); final SpecificationEntity se = new ReturnValue(methodName, packageName, className, type); handles2categories.put(tmpHandle, category); - tmpMap.put(se, new Pair<>(tmpHandle, category)); + tmpMap.put(se, new Pair(tmpHandle, category)); } private void putFlow(Attributes attributes) { @@ -196,6 +212,7 @@ private void checkDomainAssignmentsWithFlows() { */ } + @SuppressWarnings("nullness") private void checkFlows() { for (var p : categories2domains.entrySet()) { assert domains.contains(categories2domains.get(p.getKey())); @@ -203,7 +220,7 @@ private void checkFlows() { } @Override - public void startElement(String uri, String localName, String qName, Attributes attributes) { + public void startElement(String uri, String localName, String qName, Attributes attributes) throws SAXException { switch (localName) { case "sourcedompair", "source" -> startSources(); case "sinkdompair", "sink" -> startSinks(); diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java index d76a95c697a..1cc90609899 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java +++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java @@ -117,7 +117,7 @@ public static File getDefaultSavePath(File origSourcePath) { private static File getBaseDirPath(File origSourcePath) { if (origSourcePath.isFile()) { - return origSourcePath.getParentFile(); + return Objects.requireNonNull(origSourcePath.getParentFile()); } else { return origSourcePath; } diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationEntity.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationEntity.java index b472160ddaa..7cd4b1118d6 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationEntity.java +++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationEntity.java @@ -13,7 +13,7 @@ */ public abstract class SpecificationEntity { - enum Type { + public enum Type { SOURCE, SINK } @@ -34,7 +34,7 @@ public static final class Field extends SpecificationEntity { } @Override - public boolean equals(Object o) { + public boolean equals(@org.jspecify.annotations.Nullable Object o) { if (super.equals(o) && o instanceof Field) { return name.equals(((Field) o).name); } else { @@ -92,7 +92,7 @@ public static final class Parameter extends SpecificationEntity { } @Override - public boolean equals(Object o) { + public boolean equals(@org.jspecify.annotations.Nullable Object o) { if (super.equals(o) && o instanceof Parameter) { return (methodName.equals(((Parameter) o).methodName) && Arrays.equals(((Parameter) o).paramTypes, paramTypes) @@ -164,7 +164,7 @@ public static final class ReturnValue extends SpecificationEntity { } @Override - public boolean equals(Object o) { + public boolean equals(@org.jspecify.annotations.Nullable Object o) { if (super.equals(o) && o instanceof ReturnValue) { return (methodName.equals(((ReturnValue) o).methodName) && Arrays.equals(paramTypes, ((ReturnValue) o).paramTypes)); @@ -209,7 +209,7 @@ private SpecificationEntity(String p, String c, Type t) { } @Override - public boolean equals(Object o) { + public boolean equals(@org.jspecify.annotations.Nullable Object o) { if (o instanceof SpecificationEntity) { return (inPackage.equals(((SpecificationEntity) o).inPackage) && inClass.equals(((SpecificationEntity) o).inClass) diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationInjector.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationInjector.java index 3f5b700be8b..4a623414369 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationInjector.java +++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/SpecificationInjector.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.util.rifl.SpecificationEntity.Type; +import org.jspecify.annotations.Nullable; import recoder.abstraction.ClassType; import recoder.java.*; import recoder.java.declaration.*; @@ -49,18 +50,13 @@ private static class JMLFactory { private final String indentation; private final Map>> respects = new HashMap<>(); - private SpecificationContainer sc; + private final SpecificationContainer sc; JMLFactory(SpecificationContainer sc) { indentation = DEFAULT_INDENTATION; this.sc = sc; } - @SuppressWarnings("unused") - JMLFactory(int indent) { - indentation = " ".repeat(indent); - } - @SuppressWarnings("unused") void addResultToDetermines(Type t) { put(DEFAULT_KEY, t, RESULT); @@ -85,7 +81,7 @@ void addToDetermines(String name, Type t, String key) { } String getRespects(String domain, final Type t) { - return getRespects(respects.get(domain), t); + return getRespects(Objects.requireNonNull(respects.get(domain)), t); } String getRespects(Set oneRespect) { @@ -157,13 +153,13 @@ String getSpecification() { sb.append(JML_END); return sb.toString(); } else { - return null; + return ""; } } - private void put(String key, Entry value) { + private void put(@Nullable String key, Entry value) { if (key == null) { return; } @@ -206,7 +202,7 @@ private void accessChildren(JavaNonTerminalProgramElement pe) { } } - private void addComment(JavaProgramElement se, String comment) { + private void addComment(JavaProgramElement se, @Nullable String comment) { // remember which methods were specified and generate po files only for them if (se instanceof MethodDeclaration) { specifiedMethodDeclarations.add((MethodDeclaration) se); diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java index 49bbd163229..665c71d3799 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java +++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java @@ -5,4 +5,7 @@ * This package contains a transformer from input RIFL files (XML) and * original Java files to JML* annotated files. */ +@NullMarked package de.uka.ilkd.key.util.rifl; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java index e04c2be2a75..202af63ddbb 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java @@ -1046,7 +1046,7 @@ public String toString() { * {@inheritDoc} */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof ExtractLocationParameter other) { return Objects.equals(arrayIndex, other.arrayIndex) && stateMember == other.stateMember @@ -1775,7 +1775,7 @@ public Node getGoalNode() { * {@inheritDoc} */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof ExecutionVariableValuePair other) { return isArrayRange() ? (getArrayStartIndex().equals(other.getArrayStartIndex()) diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionVariableExtractor.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionVariableExtractor.java index 904292a5548..da383736830 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionVariableExtractor.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionVariableExtractor.java @@ -335,7 +335,7 @@ private record ParentDef(Term parent, Node goalNode) { * {@inheritDoc} */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof ParentDef other) { return Objects.equals(parent, other.parent) && Objects.equals(goalNode, other.goalNode); @@ -369,7 +369,7 @@ private record LocationDef(ProgramVariable programVariable, Term arrayIndex) { * {@inheritDoc} */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof LocationDef other) { return programVariable == other.programVariable && Objects.equals(arrayIndex, other.arrayIndex); diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java index 35e6ea1b81d..59ea11da510 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java @@ -1850,7 +1850,7 @@ public JavaPair(Integer stackSize, ImmutableList elementsOfIntere * {@inheritDoc} */ @Override - public boolean equals(Object o) { + public boolean equals(@org.jspecify.annotations.Nullable Object o) { if (super.equals(o)) { if (o instanceof JavaPair other) { if (second.size() == other.second.size()) { diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java index 726d64d25fa..3b3bd842851 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java @@ -245,7 +245,7 @@ public int hashCode() { * {@inheritDoc} */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof ProgramMethodPO other) { return Objects.equals(pm, other.getProgramMethod()) && Objects.equals(precondition, other.getPrecondition()); diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java index 46547b4935b..adf799c9770 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java @@ -284,7 +284,7 @@ public int hashCode() { * {@inheritDoc} */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof ProgramMethodSubsetPO other) { return super.equals(obj) && Objects.equals(getStartPosition(), other.getStartPosition()) diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Access.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Access.java index b9f0b4690f4..81fe0db08fa 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Access.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Access.java @@ -97,7 +97,7 @@ public int hashCode() { * {@inheritDoc} */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof Access other) { return Objects.equals(programVariable, other.getProgramVariable()) && Objects.equals(dimensionExpressions, other.getDimensionExpressions()); diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Location.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Location.java index 3091bad94d2..1944dcf6854 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Location.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Location.java @@ -78,7 +78,7 @@ public int hashCode() { * {@inheritDoc} */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof Location other) { return Objects.equals(accesses, other.getAccesses()); } else { diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/EqualsHashCodeResetter.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/EqualsHashCodeResetter.java index 235a298b454..41934f88562 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/EqualsHashCodeResetter.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/EqualsHashCodeResetter.java @@ -41,7 +41,7 @@ public record EqualsHashCodeResetter(T wrappedElement) { * Overwritten to restore default Java implementation with reference based equality. */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof EqualsHashCodeResetter) { return wrappedElement() == ((EqualsHashCodeResetter) obj).wrappedElement(); } else { diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestEqualsHashCodeResetter.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestEqualsHashCodeResetter.java index 400e76423ef..a7442b5aa93 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestEqualsHashCodeResetter.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestEqualsHashCodeResetter.java @@ -252,7 +252,7 @@ private record MyBean(String value) { * Overwritten to make {@link MyBean}s equal if they have the same value. */ @Override - public boolean equals(Object obj) { + boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (obj instanceof MyBean) { return value.equals(((MyBean) obj).value); } else { diff --git a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceOfNotInEndlessLoop/test/Number.java b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceOfNotInEndlessLoop/test/Number.java index 1348e65badd..3524ba2fff5 100644 --- a/key.core.symbolic_execution/src/test/resources/testcase/set/instanceOfNotInEndlessLoop/test/Number.java +++ b/key.core.symbolic_execution/src/test/resources/testcase/set/instanceOfNotInEndlessLoop/test/Number.java @@ -5,7 +5,7 @@ public class Number { @ requires true; @ ensures true; @*/ - public boolean equals(Object n) { + boolean equals(@org.jspecify.annotations.Nullable Object n) { if (n instanceof Number) { if (content == ((Number) n).content) { return true; diff --git a/key.core.testgen/build.gradle b/key.core.testgen/build.gradle index 771d651021a..5afeced047b 100644 --- a/key.core.testgen/build.gradle +++ b/key.core.testgen/build.gradle @@ -3,3 +3,19 @@ description "Test Case Generation based on proof attempts." dependencies { implementation project(":key.core") } + +checkerFramework { + if (System.getProperty("ENABLE_NULLNESS")) { + checkers = [ + "org.checkerframework.checker.nullness.NullnessChecker", + ] + extraJavacArgs = [ + //"-AonlyDefs=^org\\.key_project\\.logic", + "-Xmaxerrs", "10000", + "-Astubs=$rootDir/key.util/src/main/checkerframework${File.pathSeparatorChar}permit-nullness-assertion-exception.astub", + "-AstubNoWarnIfNotFound", + "-Werror", + "-Aversion", + ] + } +} diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/SemanticsBlastingMacro.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/SemanticsBlastingMacro.java index 30e2db9dc14..646236e53d2 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/SemanticsBlastingMacro.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/SemanticsBlastingMacro.java @@ -70,7 +70,7 @@ public String getName() { @Override public String getCategory() { - return null; + return ""; } @Override diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java index 8a5da4014c5..c58e83a894f 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.macros; import java.util.HashSet; +import java.util.Objects; import java.util.Set; import de.uka.ilkd.key.logic.PosInOccurrence; @@ -20,10 +21,12 @@ import org.key_project.logic.Name; +import org.jspecify.annotations.Nullable; + public class TestGenMacro extends StrategyProofMacro { @Override protected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc) { - return new TestGenStrategy(proof.getActiveStrategy()); + return new TestGenStrategy(Objects.requireNonNull(proof.getActiveStrategy())); } @Override @@ -38,7 +41,7 @@ public String getName() { @Override public String getCategory() { - return null; + return ""; } @@ -54,8 +57,11 @@ class TestGenStrategy extends FilterStrategy { private static final Set unwindRules; private static final int UNWIND_COST = 1000; private final int limit; - /** the modality cache used by this strategy */ + /** + * the modality cache used by this strategy + */ private final ModalityCache modalityCache = new ModalityCache(); + static { unwindRules = new HashSet<>(); TestGenStrategy.unwindRules.add("loopUnwind"); @@ -66,7 +72,7 @@ class TestGenStrategy extends FilterStrategy { TestGenStrategy.unwindRules.add("staticMethodCallWithAssignment"); } - private static boolean isUnwindRule(Rule rule) { + private static boolean isUnwindRule(@Nullable Rule rule) { if (rule == null) { return false; } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/package-info.java new file mode 100644 index 00000000000..91bba9d9a99 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (23.01.25) + */ +@NullMarked +package de.uka.ilkd.key.macros; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java index 00f24ad3c1f..cd0e7f78362 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java @@ -84,15 +84,7 @@ public TestGenerationSettings(TestGenerationSettings data) { } - /** - * @deprecated weigl: This method seems broken. I would expect: clone() = new TGS(this) - */ - @Deprecated(forRemoval = true) - public TestGenerationSettings clone(TestGenerationSettings data) { - return new TestGenerationSettings(data); - } - - public TestGenerationSettings clone() { + public TestGenerationSettings copy() { return new TestGenerationSettings(this); } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/package-info.java new file mode 100644 index 00000000000..fdc268f615d --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (23.01.25) + */ +@NullMarked +package de.uka.ilkd.key.settings; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/package-info.java new file mode 100644 index 00000000000..0786cfcf9d3 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (23.01.25) + */ +@NullMarked +package de.uka.ilkd.key.smt.counterexample; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/package-info.java new file mode 100644 index 00000000000..3dd3cc20f81 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (23.01.25) + */ +@NullMarked +package de.uka.ilkd.key.smt; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java index 2fbfc7b1ce4..9e728520afb 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java @@ -42,6 +42,7 @@ import de.uka.ilkd.key.util.ProofStarter; import de.uka.ilkd.key.util.SideProofUtil; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; import org.slf4j.Logger; @@ -57,8 +58,8 @@ public abstract class AbstractTestGenerator { private static final Logger LOGGER = LoggerFactory.getLogger(AbstractTestGenerator.class); private final UserInterfaceControl ui; private final Proof originalProof; - private SolverLauncher launcher; - private List proofs; + private @Nullable SolverLauncher launcher; + private @Nullable List proofs; /** * Constructor. @@ -72,11 +73,8 @@ protected AbstractTestGenerator(UserInterfaceControl ui, Proof originalProof) { } public void generateTestCases(final StopRequest stopRequest, final TestGenerationLog log) { - - TestGenerationSettings settings = TestGenerationSettings.getInstance(); - if (!SolverTypes.Z3_CE_SOLVER.isInstalled(true)) { log.writeln("Could not find the z3 SMT solver. Aborting."); return; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/package-info.java new file mode 100644 index 00000000000..d7397e7c087 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (23.01.25) + */ +@NullMarked +package de.uka.ilkd.key.smt.testgen; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java index ed33123fa61..c27ac14dca5 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java @@ -22,6 +22,7 @@ import org.key_project.logic.sort.Sort; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -37,7 +38,7 @@ public ProofInfo(Proof proof) { this.services = proof.getServices(); } - public IProgramMethod getMUT() { + public @Nullable IProgramMethod getMUT() { SpecificationRepository spec = services.getSpecificationRepository(); IObserverFunction f = spec.getTargetOfProof(proof); if (f instanceof IProgramMethod) { @@ -47,7 +48,7 @@ public IProgramMethod getMUT() { } } - public KeYJavaType getTypeOfClassUnderTest() { + public @Nullable KeYJavaType getTypeOfClassUnderTest() { if (getMUT() == null) { return null; } @@ -180,7 +181,7 @@ private String processUpdate(Term update) { return result.toString(); } - public JavaBlock getJavaBlock(Term t) { + public @Nullable JavaBlock getJavaBlock(Term t) { if (t.containsJavaBlockRecursive()) { if (!t.javaBlock().isEmpty()) { return t.javaBlock(); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java index 3b0112a4f05..380f5cf9f98 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java @@ -215,7 +215,7 @@ public String getMUTCall() { params.append(",").append(var.name()); } } - if (params.length() > 0) { + if (!params.isEmpty()) { params = new StringBuilder(params.substring(1)); } @@ -330,8 +330,7 @@ protected String buildDummyClassForAbstractSort(Sort sort) { sb.append("{ return \"").append(className).append("\";}"); returnNull = false; } - } catch (final Exception e) { - returnNull = true; + } catch (final Exception ignored) { } if (returnNull) { sb.append("{ return null;}"); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocation.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocation.java index c7190509695..91f578aa97a 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocation.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleLocation.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.testgen.oracle; +import org.jspecify.annotations.Nullable; + public class OracleLocation { public static final String ALL_FIELDS = ""; @@ -35,14 +37,13 @@ public boolean isAllFields() { return field.equals(ALL_FIELDS); } - public boolean equals(Object o) { - + @Override + public boolean equals(@Nullable Object o) { if (o instanceof OracleLocation l) { return object.equals(l.object) && field.equals(l.field); } return false; - } public String toString() { diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleVariable.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleVariable.java index 4fd6805b7fe..a2e591d2f07 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleVariable.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleVariable.java @@ -8,7 +8,7 @@ public record OracleVariable(String name, Sort sort) implements OracleTerm { @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (this == obj) { return true; } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/package-info.java new file mode 100644 index 00000000000..0051f90f6ed --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (23.01.25) + */ +@NullMarked +package de.uka.ilkd.key.testgen.oracle; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/package-info.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/package-info.java new file mode 100644 index 00000000000..cea7b85d606 --- /dev/null +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (23.01.25) + */ +@NullMarked +package de.uka.ilkd.key.testgen; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core/build.gradle b/key.core/build.gradle index 054104438c0..50c13de2d3b 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -266,3 +266,26 @@ task generateRAPUnitTests(type: JavaExec) { sourceSets.test.java.srcDirs("$buildDir/generated-src/rap/") sourcesJar.dependsOn(runAntlr4Jml, runAntlr4Key, compileJavacc, generateGrammarSource) + + +checkerFramework { + if(System.getProperty("ENABLE_NULLNESS")) { + checkers = [ + "org.checkerframework.checker.nullness.NullnessChecker", + ] + extraJavacArgs = [ + ///home/weigl/work/key/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp + //"-AonlyDefs=^de\\.uka\\.ilkd\\.key\\.(nparser\\.varexp|ldt|util|proof|control|macros|settings)(\\.*)?", + //"-AonlyDefs=^de\\.uka\\.ilkd\\.key\\.proof(\\.*)?", + "-AonlyDefs=^de\\.uka\\.ilkd\\.key\\.util(\\.*)?", + "-AassumeAssertionsAreEnabled", + "-AassumePureGetters", + "-AassumeInitialized", + "-Xmaxerrs", "10000", + "-Astubs=$rootDir/key.util/src/main/checkerframework${File.pathSeparatorChar}permit-nullness-assertion-exception.astub", + "-AstubNoWarnIfNotFound", + "-Werror", + "-Aversion", + ] + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/KeYApi.java b/key.core/src/main/java/de/uka/ilkd/key/api/KeYApi.java index dc89908c39c..4099c621bac 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/api/KeYApi.java +++ b/key.core/src/main/java/de/uka/ilkd/key/api/KeYApi.java @@ -10,6 +10,8 @@ import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.util.KeYConstants; +import org.jspecify.annotations.Nullable; + /** * The Entry Point. *

@@ -33,7 +35,6 @@ private KeYApi() { } /** - * * @return */ public static String getVersion() { @@ -72,8 +73,10 @@ public static ProofManagementApi loadFromKeyFile(File keyFile) throws ProblemLoa * @return * @throws ProblemLoaderException */ - public static ProofManagementApi loadProof(File location, List classPath, - File bootClassPath, List includes) throws ProblemLoaderException { + public static ProofManagementApi loadProof(File location, + @Nullable List classPath, + @Nullable File bootClassPath, + @Nullable List includes) throws ProblemLoaderException { return new ProofManagementApi( KeYEnvironment.load(location, classPath, bootClassPath, includes)); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/ScriptResults.java b/key.core/src/main/java/de/uka/ilkd/key/api/ScriptResults.java index efc2bb66b2f..b816f36bd02 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/api/ScriptResults.java +++ b/key.core/src/main/java/de/uka/ilkd/key/api/ScriptResults.java @@ -97,7 +97,7 @@ public void clear() { } @Override - public boolean equals(Object o) { + public boolean equals(@org.jspecify.annotations.Nullable Object o) { return delegated.equals(o); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/boollattice/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/boollattice/package-info.java new file mode 100644 index 00000000000..6f6d5b32744 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/boollattice/package-info.java @@ -0,0 +1,8 @@ +/** + * This package contains the core data structures of proofs, nodes, goals, as well + * as machinery to deal with these data structures. + */ +@NullMarked +package de.uka.ilkd.key.axiom_abstraction.boollattice; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/package-info.java new file mode 100644 index 00000000000..a2a3468ff9b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/package-info.java @@ -0,0 +1,8 @@ +/** + * This package contains the core data structures of proofs, nodes, goals, as well + * as machinery to deal with these data structures. + */ +@NullMarked +package de.uka.ilkd.key.axiom_abstraction; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractPredicateAbstractionDomainElement.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractPredicateAbstractionDomainElement.java index 86e493d7e33..e44d9eaecb1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractPredicateAbstractionDomainElement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractPredicateAbstractionDomainElement.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.axiom_abstraction.predicateabstraction; import java.util.Iterator; +import java.util.Objects; import de.uka.ilkd.key.axiom_abstraction.AbstractDomainElement; import de.uka.ilkd.key.java.Services; @@ -14,6 +15,8 @@ import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; +import org.jspecify.annotations.Nullable; + /** * A base class for abstract domain elements in a predicate abstraction lattice. * @@ -21,7 +24,7 @@ */ public abstract class AbstractPredicateAbstractionDomainElement extends AbstractDomainElement { - private ImmutableSet predicates = null; + private ImmutableSet predicates; private boolean topElem = false; /** @@ -29,7 +32,7 @@ public abstract class AbstractPredicateAbstractionDomainElement extends Abstract * abstraction predicates. */ public AbstractPredicateAbstractionDomainElement( - final ImmutableSet predicates) { + ImmutableSet predicates) { this.predicates = predicates; } @@ -75,7 +78,7 @@ public Name name() { return new Name("TOP"); } - if (predicates.size() == 0) { + if (predicates.isEmpty()) { return new Name("BOTTOM"); } @@ -111,7 +114,7 @@ public Term getDefiningAxiom(Term varOrConst, Services services) { return tb.tt(); } - if (predicates.size() == 0) { + if (predicates.isEmpty()) { return tb.ff(); } @@ -125,7 +128,7 @@ public Term getDefiningAxiom(Term varOrConst, Services services) { } } - return result; + return Objects.requireNonNull(result); } /** @@ -165,7 +168,7 @@ public String toParseableString(Services services) { } @Override - public abstract boolean equals(Object obj); + public abstract boolean equals(@Nullable Object obj); @Override public abstract int hashCode(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractionPredicate.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractionPredicate.java index 1ad934571b8..1098c9ad366 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractionPredicate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractionPredicate.java @@ -5,6 +5,7 @@ import java.util.ArrayList; import java.util.List; +import java.util.Objects; import java.util.function.Function; import java.util.regex.Matcher; import java.util.regex.Pattern; @@ -24,6 +25,8 @@ import org.key_project.logic.sort.Sort; import org.key_project.util.collection.Pair; +import org.jspecify.annotations.Nullable; + /** * Interface for predicates used for predicate abstraction. An abstraction predicate is a mapping * from program variables or constants to formulae instantiated for the respective variable. @@ -44,7 +47,7 @@ public abstract class AbstractionPredicate implements Function, Name * * This field is needed to save proofs with abstraction predicates. */ - private Term predicateFormWithPlaceholder = null; + private Term predicateFormWithPlaceholder; /** * The placeholder variable occurring in {@link #predicateFormWithPlaceholder} which is to be @@ -53,7 +56,7 @@ public abstract class AbstractionPredicate implements Function, Name * * This field is needed to save proofs with abstraction predicates.s */ - private LocationVariable placeholderVariable = null; + private LocationVariable placeholderVariable; /** * Creates a new {@link AbstractionPredicate}. Constructor is hidden since elements fo this @@ -116,8 +119,8 @@ public static AbstractionPredicate create(final Term predicate, final Sort fInputSort = placeholder.sort(); AbstractionPredicate result = new AbstractionPredicate(fInputSort) { - private final Name name = new Name("abstrPred_" + predicate.op().toString()); - private Function mapping = null; + private final Name name = new Name("abstrPred_" + predicate.op()); + private @Nullable Function mapping = null; @Override public Term apply(Term input) { @@ -220,8 +223,8 @@ public static List fromString(final String s, final Servic assert i + 1 <= m.groupCount() : "Wrong format of join abstraction predicates: " + "There should always be pairs of placeholders and predicate terms."; - final String phStr = m.group(i); - final String predStr = m.group(i + 1); + final String phStr = Objects.requireNonNull(m.group(i)); + final String predStr = Objects.requireNonNull(m.group(i + 1)); // Parse the placeholder Pair ph = MergeRuleUtils.parsePlaceholder(phStr, false, services); @@ -247,13 +250,14 @@ public static List fromString(final String s, final Servic } @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { if (!(obj instanceof AbstractionPredicate otherPred)) { return false; } - return otherPred.placeholderVariable.equals(placeholderVariable) - && otherPred.predicateFormWithPlaceholder.equals(predicateFormWithPlaceholder); + return Objects.equals(otherPred.placeholderVariable, placeholderVariable) + && Objects.equals(otherPred.predicateFormWithPlaceholder, + predicateFormWithPlaceholder); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionDomainElement.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionDomainElement.java index e4004bc1fad..ae51d451c93 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionDomainElement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionDomainElement.java @@ -62,7 +62,7 @@ public String getPredicateNameCombinationString() { * @see java.lang.Object#equals(java.lang.Object) */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { return obj instanceof ConjunctivePredicateAbstractionDomainElement && (this != TOP || obj == TOP) && (this != BOTTOM || obj == BOTTOM) && this.getPredicates().equals( diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionLattice.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionLattice.java index da23857e09a..f0b065c079f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionLattice.java +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionLattice.java @@ -89,7 +89,7 @@ public int size() { * @see java.lang.Object#equals(java.lang.Object) */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { return obj instanceof ConjunctivePredicateAbstractionLattice && ((ConjunctivePredicateAbstractionLattice) obj).predicates .equals(this.predicates); diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionDomainElement.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionDomainElement.java index 9c4f1ed4f37..598ac59181c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionDomainElement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionDomainElement.java @@ -62,7 +62,7 @@ public String getPredicateNameCombinationString() { * @see java.lang.Object#equals(java.lang.Object) */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { return obj instanceof DisjunctivePredicateAbstractionDomainElement && (this != TOP || obj == TOP) && (this != BOTTOM || obj == BOTTOM) && this.getPredicates().equals( diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionLattice.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionLattice.java index 1350b4a5bae..acea17bf9a0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionLattice.java +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionLattice.java @@ -87,7 +87,7 @@ public int size() { * @see java.lang.Object#equals(java.lang.Object) */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { return obj instanceof DisjunctivePredicateAbstractionLattice && ((DisjunctivePredicateAbstractionLattice) obj).predicates .equals(this.predicates); diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionDomainElement.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionDomainElement.java index b97f4b38cdf..6b8fce52f01 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionDomainElement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionDomainElement.java @@ -63,7 +63,7 @@ public String getPredicateNameCombinationString() { * @see java.lang.Object#equals(java.lang.Object) */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { return obj instanceof SimplePredicateAbstractionDomainElement && (this != TOP || obj == TOP) && (this != BOTTOM || obj == BOTTOM) && this.getPredicates() .equals(((SimplePredicateAbstractionDomainElement) obj).getPredicates()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionLattice.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionLattice.java index 9ea5c73a491..5c29a7dc277 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionLattice.java +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionLattice.java @@ -101,7 +101,7 @@ public int size() { * @see java.lang.Object#equals(java.lang.Object) */ @Override - public boolean equals(Object obj) { + public boolean equals(@org.jspecify.annotations.Nullable Object obj) { return obj instanceof SimplePredicateAbstractionLattice && ((SimplePredicateAbstractionLattice) obj).predicates.equals(this.predicates); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/package-info.java new file mode 100644 index 00000000000..c438cd4c95b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/package-info.java @@ -0,0 +1,8 @@ +/** + * This package contains the core data structures of proofs, nodes, goals, as well + * as machinery to deal with these data structures. + */ +@NullMarked +package de.uka.ilkd.key.axiom_abstraction.predicateabstraction; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/signanalysis/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/signanalysis/package-info.java new file mode 100644 index 00000000000..7497de227b1 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/signanalysis/package-info.java @@ -0,0 +1,8 @@ +/** + * This package contains the core data structures of proofs, nodes, goals, as well + * as machinery to deal with these data structures. + */ +@NullMarked +package de.uka.ilkd.key.axiom_abstraction.signanalysis; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java index 0d3fd45622c..28a63d91589 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java @@ -27,6 +27,7 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -41,7 +42,7 @@ public abstract class AbstractProofControl implements ProofControl { /** * Optionally, the {@link RuleCompletionHandler} to use. */ - private final RuleCompletionHandler ruleCompletionHandler; + private final @Nullable RuleCompletionHandler ruleCompletionHandler; /** * The default {@link ProverTaskListener} which will be added to all started @@ -79,7 +80,7 @@ public AbstractProofControl(ProverTaskListener defaultProverTaskListener) { * @param ruleCompletionHandler An optional {@link RuleCompletionHandler}. */ public AbstractProofControl(ProverTaskListener defaultProverTaskListener, - RuleCompletionHandler ruleCompletionHandler) { + @Nullable RuleCompletionHandler ruleCompletionHandler) { this.ruleCompletionHandler = ruleCompletionHandler; this.defaultProverTaskListener = defaultProverTaskListener; } @@ -150,7 +151,7 @@ public ImmutableList getRewriteTaclet(Goal focusedGoal, PosInOccurren * TacletApps */ private ImmutableList filterTaclet(Goal focusedGoal, - ImmutableList tacletInstances, PosInOccurrence pos) { + ImmutableList tacletInstances, @Nullable PosInOccurrence pos) { java.util.HashSet applicableRules = new java.util.HashSet<>(); ImmutableList result = ImmutableSLList.nil(); for (NoPosTacletApp app : tacletInstances) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java index ef7a1e8c6fa..9c28f1774ff 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java @@ -27,6 +27,7 @@ import de.uka.ilkd.key.prover.TaskFinishedInfo; import de.uka.ilkd.key.prover.TaskStartedInfo; +import org.jspecify.annotations.Nullable; import org.slf4j.LoggerFactory; /** @@ -205,10 +206,14 @@ public void taskFinished(TaskFinishedInfo info) { * {@inheritDoc} */ @Override - public AbstractProblemLoader load(Profile profile, File file, List classPath, - File bootClassPath, List includes, Properties poPropertiesToForce, + public AbstractProblemLoader load(@Nullable Profile profile, + @Nullable File file, + @Nullable List classPath, + @Nullable File bootClassPath, + @Nullable List includes, + @Nullable Properties poPropertiesToForce, boolean forceNewProfileOfNewProofs, - Consumer callback) throws ProblemLoaderException { + @Nullable Consumer callback) throws ProblemLoaderException { AbstractProblemLoader loader = null; try { loader = new SingleThreadProblemLoader(file, classPath, bootClassPath, includes, @@ -255,7 +260,8 @@ public void loadingStarted(AbstractProblemLoader loader) { @Override public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poContainer, - ProofAggregate proofList, ReplayResult result) throws ProblemLoaderException { + @Nullable ProofAggregate proofList, @Nullable ReplayResult result) + throws ProblemLoaderException { if (proofList != null) { // avoid double registration at spec repos as that is done already earlier in // createProof diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java index df59e0c1ae7..9e5bd329289 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/DefaultProofControl.java @@ -19,6 +19,8 @@ import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; + /** * The default implementation of {@link ProofControl}. * @@ -33,7 +35,7 @@ public class DefaultProofControl extends AbstractProofControl { /** * The currently running {@link Thread}. */ - private Thread autoModeThread; + private @Nullable Thread autoModeThread; /** * Constructor. @@ -74,7 +76,7 @@ public synchronized void startAutoMode(Proof proof, ImmutableList goals, @Override public synchronized void stopAutoMode() { - if (isInAutoMode()) { + if (isInAutoMode() && autoModeThread != null) { autoModeThread.interrupt(); } } @@ -111,10 +113,8 @@ public AutoModeThread(Proof proof, ImmutableList goals, ProverTaskListener public void run() { try { fireAutoModeStarted(new ProofEvent(proof)); - ProofStarter starter = ptl != null - ? new ProofStarter( - new CompositePTListener(getDefaultProverTaskListener(), ptl), false) - : new ProofStarter(getDefaultProverTaskListener(), false); + ProofStarter starter = new ProofStarter( + new CompositePTListener(getDefaultProverTaskListener(), ptl), false); starter.init(proof); if (goals != null) { starter.start(goals); diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/DefaultUserInterfaceControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/DefaultUserInterfaceControl.java index 28861ebe15d..1acc0f67de1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/DefaultUserInterfaceControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/DefaultUserInterfaceControl.java @@ -11,6 +11,8 @@ import org.key_project.util.collection.ImmutableSet; +import org.jspecify.annotations.Nullable; + /** * The {@link DefaultUserInterfaceControl} which allows proving in case that no specific user * interface is available. @@ -45,7 +47,7 @@ public DefaultUserInterfaceControl() { * * @param customization An optional {@link RuleCompletionHandler}. */ - public DefaultUserInterfaceControl(RuleCompletionHandler customization) { + public DefaultUserInterfaceControl(@Nullable RuleCompletionHandler customization) { proofControl = new DefaultProofControl(this, this, customization); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java index bc34b6eaf8a..3d0d910c44f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java @@ -43,7 +43,7 @@ public class KeYEnvironment { /** * An optional {@link Proof} which was loaded by the specified proof file. */ - private final Proof loadedProof; + private final @Nullable Proof loadedProof; /** * An optional field denoting a script contained in the proof file. @@ -58,7 +58,7 @@ public class KeYEnvironment { /** * The {@link ReplayResult} if available. */ - private final ReplayResult replayResult; + private final @Nullable ReplayResult replayResult; /** * Constructor @@ -76,8 +76,8 @@ public KeYEnvironment(U ui, InitConfig initConfig) { * @param ui The {@link UserInterfaceControl} in which the {@link Proof} is loaded. * @param initConfig The loaded project. */ - public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof, - @Nullable ProofScriptEntry proofScript, ReplayResult replayResult) { + public KeYEnvironment(U ui, InitConfig initConfig, @Nullable Proof loadedProof, + @Nullable ProofScriptEntry proofScript, @Nullable ReplayResult replayResult) { this.ui = ui; this.initConfig = initConfig; this.loadedProof = loadedProof; @@ -100,7 +100,7 @@ public U getUi() { * @return The {@link ProofControl} of {@link #getUi()}. */ public ProofControl getProofControl() { - return ui != null ? ui.getProofControl() : null; + return ui.getProofControl(); } /** @@ -148,7 +148,7 @@ public Profile getProfile() { * * @return The loaded {@link Proof} if available and {@code null} otherwise. */ - public Proof getLoadedProof() { + public @Nullable Proof getLoadedProof() { return loadedProof; } @@ -157,7 +157,7 @@ public Proof getLoadedProof() { * * @return The {@link ReplayResult} or {@code null} if not available. */ - public ReplayResult getReplayResult() { + public @Nullable ReplayResult getReplayResult() { return replayResult; } @@ -184,7 +184,8 @@ public Proof createProof(ProofOblInput input) throws ProofInputException { * @throws ProblemLoaderException Occurred Exception */ public static KeYEnvironment load(File location, - List classPaths, File bootClassPath, List includes) + @Nullable List classPaths, @Nullable File bootClassPath, + @Nullable List includes) throws ProblemLoaderException { return load(null, location, classPaths, bootClassPath, includes, false); } @@ -224,8 +225,10 @@ public static KeYEnvironment load(File location, * @return The {@link KeYEnvironment} which contains all references to the loaded location. * @throws ProblemLoaderException Occurred Exception */ - public static KeYEnvironment load(Profile profile, File location, - List classPaths, File bootClassPath, List includes, + public static KeYEnvironment load(@Nullable Profile profile, + File location, + @Nullable List classPaths, + @Nullable File bootClassPath, @Nullable List includes, boolean forceNewProfileOfNewProofs) throws ProblemLoaderException { return load(profile, location, classPaths, bootClassPath, includes, null, null, forceNewProfileOfNewProofs); @@ -249,9 +252,13 @@ public static KeYEnvironment load(Profile profile, * @return The {@link KeYEnvironment} which contains all references to the loaded location. * @throws ProblemLoaderException Occurred Exception */ - public static KeYEnvironment load(Profile profile, File location, - List classPaths, File bootClassPath, List includes, - Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler, + public static KeYEnvironment load(@Nullable Profile profile, + File location, + @Nullable List classPaths, + @Nullable File bootClassPath, + @Nullable List includes, + @Nullable Properties poPropertiesToForce, + @Nullable RuleCompletionHandler ruleCompletionHandler, boolean forceNewProfileOfNewProofs) throws ProblemLoaderException { return load(profile, location, classPaths, bootClassPath, includes, poPropertiesToForce, ruleCompletionHandler, @@ -278,10 +285,14 @@ public static KeYEnvironment load(Profile profile, * @return The {@link KeYEnvironment} which contains all references to the loaded location. * @throws ProblemLoaderException Occurred Exception */ - public static KeYEnvironment load(Profile profile, File location, - List classPaths, File bootClassPath, List includes, - Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler, - Consumer callbackProofLoaded, + public static KeYEnvironment load(@Nullable Profile profile, + File location, + @Nullable List classPaths, + @Nullable File bootClassPath, + @Nullable List includes, + @Nullable Properties poPropertiesToForce, + @Nullable RuleCompletionHandler ruleCompletionHandler, + @Nullable Consumer callbackProofLoaded, boolean forceNewProfileOfNewProofs) throws ProblemLoaderException { DefaultUserInterfaceControl ui = new DefaultUserInterfaceControl(ruleCompletionHandler); AbstractProblemLoader loader = ui.load(profile, location, classPaths, bootClassPath, @@ -311,7 +322,7 @@ public void dispose() { * Checks if this {@link KeYEnvironment} is disposed meaning that {@link #dispose()} was already * executed at least once. * - * @return {@code true} disposed, {@code false} not disposed and still functionable. + * @return {@code true} disposed, {@code false} not disposed and still functional. */ public boolean isDisposed() { return disposed; diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/UserInterfaceControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/UserInterfaceControl.java index e7a9f1d26db..8dc3b96fd98 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/UserInterfaceControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/UserInterfaceControl.java @@ -19,6 +19,8 @@ import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.prover.ProverTaskListener; +import org.jspecify.annotations.Nullable; + /** * Provides the user interface independent logic to manage multiple proofs. This includes: *