diff --git a/build.gradle b/build.gradle index d19a3c4d438..0c021e8ae75 100644 --- a/build.gradle +++ b/build.gradle @@ -92,11 +92,11 @@ subprojects { //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:1.0.0") + implementation("org.jspecify:jspecify:1.0.0") testCompileOnly("org.jspecify:jspecify:1.0.0") def eisop_version = "3.49.3-eisop1" - compileOnly "io.github.eisop:checker-qual:$eisop_version" - compileOnly "io.github.eisop:checker-util:$eisop_version" + implementation "io.github.eisop:checker-qual:$eisop_version" + implementation "io.github.eisop:checker-util:$eisop_version" testCompileOnly "io.github.eisop:checker-qual:$eisop_version" checkerFramework "io.github.eisop:checker-qual:$eisop_version" checkerFramework "io.github.eisop:checker:$eisop_version" @@ -138,6 +138,10 @@ subprojects { systemProperty "key.disregardSettings", "true" maxHeapSize = "4g" + // RAC non-null references. + jvmArgs("-javaagent:$rootDir/nonnull-0.1.0-SNAPSHOT-all.jar=VERBOSE,org.key_project,de.uka") + + forkEvery = 0 //default maxParallelForks = 1 // weigl: test on master } diff --git a/key.core.example/src/main/java/org/key_project/Main.java b/key.core.example/src/main/java/org/key_project/Main.java index ca565fbae3b..0a3fe798eec 100644 --- a/key.core.example/src/main/java/org/key_project/Main.java +++ b/key.core.example/src/main/java/org/key_project/Main.java @@ -23,6 +23,7 @@ import org.key_project.util.collection.ImmutableSet; +import org.jspecify.annotations.NullMarked; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -31,6 +32,7 @@ * * @author Martin Hentschel */ +@NullMarked public class Main { private static final Logger LOGGER = LoggerFactory.getLogger(Main.class); @@ -52,14 +54,12 @@ public static void main(String[] args) { } } - /** - * sets up the environment with the Java project described by its location - * - * @param location the Path with the path to the source directory of the Java project - * to be verified - * @return the {@KeYEnvironment} that provides the context for all following verification tasks - * @throws ProblemLoaderException if the setup fails - */ + /// sets up the environment with the Java project described by its location + /// + /// @param location the Path with the path to the source directory of the Java project + /// to be verified + /// @return the [KeYEnvironment] that provides the context for all following verification tasks + /// @throws ProblemLoaderException if the setup fails private static KeYEnvironment setupEnvironment(Path location) throws ProblemLoaderException { List classPaths = null; // Optionally: Additional specifications for API classes Path bootClassPath = null; // Optionally: Different default specifications for Java API @@ -77,10 +77,8 @@ private static KeYEnvironment setupEnvironment(Path location) throws ProblemL newSettings.putAll(MiscTools.getDefaultTacletOptions()); choiceSettings.setDefaultChoices(newSettings); // Load source code - KeYEnvironment env = - KeYEnvironment.load(location, classPaths, bootClassPath, includes); + return KeYEnvironment.load(location, classPaths, bootClassPath, includes); // env.getLoadedProof() returns performed proof if a *.proof file is loaded - return env; } /** @@ -93,7 +91,7 @@ private static void proveEnvironmemt(KeYEnvironment env) { final List proofContracts = getContracts(env); for (Contract contract : proofContracts) { - LOGGER.info("Found contract '" + contract.getDisplayName()); + LOGGER.info("Found contract '{}'", contract.getDisplayName()); proveContract(env, contract); } } finally { @@ -166,9 +164,8 @@ private static void proveContract(KeYEnvironment env, Contract contract) { env.getUi().getProofControl().startAndWaitForAutoMode(proof); // Show proof result boolean closed = proof.openGoals().isEmpty(); - LOGGER.info("Contract '" + contract.getDisplayName() + "' of " - + contract.getTarget() + " is " + (closed ? "verified" : "still open") - + "."); + LOGGER.info("Contract '{}' of {} is {}.", contract.getDisplayName(), + contract.getTarget(), closed ? "verified" : "still open"); } catch (ProofInputException e) { LOGGER.error("Exception at {} of {}", contract.getDisplayName(), contract.getTarget()); diff --git a/key.core.example/src/main/java/org/key_project/package-info.java b/key.core.example/src/main/java/org/key_project/package-info.java new file mode 100644 index 00000000000..afbd29b2981 --- /dev/null +++ b/key.core.example/src/main/java/org/key_project/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package org.key_project; diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/ProofReferenceUtil.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/ProofReferenceUtil.java index fd29dcf4ad0..7e30d8a1be1 100644 --- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/ProofReferenceUtil.java +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/ProofReferenceUtil.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.proof_references; import java.util.LinkedHashSet; +import java.util.Set; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.proof.Node; @@ -174,7 +175,7 @@ public static LinkedHashSet> computeProofReferences(Node node LinkedHashSet> result = new LinkedHashSet<>(); if (node != null && analysts != null) { for (IProofReferencesAnalyst analyst : analysts) { - LinkedHashSet> analystResult = + Set> analystResult = analyst.computeReferences(node, services); if (analystResult != null) { merge(result, analystResult); @@ -190,8 +191,7 @@ public static LinkedHashSet> computeProofReferences(Node node * @param target The target to add to. * @param toAdd The {@link IProofReference}s to add. */ - public static void merge(LinkedHashSet> target, - LinkedHashSet> toAdd) { + public static void merge(Set> target, Set> toAdd) { for (IProofReference reference : toAdd) { merge(target, reference); } @@ -203,7 +203,7 @@ public static void merge(LinkedHashSet> target, * @param target The target to add to. * @param reference The {@link IProofReference} to add. */ - public static void merge(LinkedHashSet> target, + public static void merge(Set> target, final IProofReference reference) { if (!target.add(reference)) { // Reference exists before, so merge nodes of both references. diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java index 8cdf5c15a71..992a329e247 100644 --- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java @@ -26,6 +26,8 @@ import org.key_project.util.collection.ImmutableSet; import org.key_project.util.collection.Pair; +import org.jspecify.annotations.Nullable; + /** * Extracts used {@link ClassAxiom} and {@link ClassInvariant}s. * @@ -36,7 +38,8 @@ public class ClassAxiomAndInvariantProofReferencesAnalyst implements IProofRefer * {@inheritDoc} */ @Override - public LinkedHashSet> computeReferences(Node node, Services services) { + public @Nullable LinkedHashSet> computeReferences(Node node, + Services services) { String name = MiscTools.getRuleName(node); if (name != null && (name.toLowerCase().contains("axiom_for") @@ -102,7 +105,7 @@ public LinkedHashSet> computeReferences(Node node, Services s * @return The {@link KeYJavaType} which provides the proof obligation or {@code null} if it was * not possible to compute it. */ - protected KeYJavaType findProofsKeYJavaType(Services services) { + protected @Nullable KeYJavaType findProofsKeYJavaType(Services services) { ProofOblInput problem = services.getSpecificationRepository().getProofOblInput(services.getProof()); if (problem != null) { diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ContractProofReferencesAnalyst.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ContractProofReferencesAnalyst.java index 6345d9615c1..8046754b9a8 100644 --- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ContractProofReferencesAnalyst.java +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ContractProofReferencesAnalyst.java @@ -12,6 +12,8 @@ import de.uka.ilkd.key.rule.AbstractContractRuleApp; import de.uka.ilkd.key.speclang.Contract; +import org.jspecify.annotations.Nullable; + /** * Extracts used contracts. * @@ -22,7 +24,8 @@ public class ContractProofReferencesAnalyst implements IProofReferencesAnalyst { * {@inheritDoc} */ @Override - public LinkedHashSet> computeReferences(Node node, Services services) { + public @Nullable LinkedHashSet> computeReferences(Node node, + Services services) { if (node.getAppliedRuleApp() instanceof AbstractContractRuleApp contractRuleApp) { DefaultProofReference reference = new DefaultProofReference<>( IProofReference.USE_CONTRACT, node, contractRuleApp.getInstantiation()); diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/IProofReferencesAnalyst.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/IProofReferencesAnalyst.java index 652233b3dea..4aa3d0751f6 100644 --- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/IProofReferencesAnalyst.java +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/IProofReferencesAnalyst.java @@ -3,13 +3,15 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof_references.analyst; -import java.util.LinkedHashSet; +import java.util.Set; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof_references.ProofReferenceUtil; import de.uka.ilkd.key.proof_references.reference.IProofReference; +import org.jspecify.annotations.Nullable; + /** *

* Instances of this class are used to compute {@link IProofReference} for a given {@link Node} @@ -34,5 +36,6 @@ public interface IProofReferencesAnalyst { * @return The found {@link IProofReference} or {@code null}/empty set if the applied rule is * not supported. */ - LinkedHashSet> computeReferences(Node node, Services services); + @Nullable + Set> computeReferences(Node node, Services services); } diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodBodyExpandProofReferencesAnalyst.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodBodyExpandProofReferencesAnalyst.java index 33c8d39990b..ce08ce3ec05 100644 --- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodBodyExpandProofReferencesAnalyst.java +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodBodyExpandProofReferencesAnalyst.java @@ -13,6 +13,8 @@ import de.uka.ilkd.key.proof_references.reference.DefaultProofReference; import de.uka.ilkd.key.proof_references.reference.IProofReference; +import org.jspecify.annotations.Nullable; + /** * Extracts inlined methods. * @@ -23,8 +25,9 @@ public class MethodBodyExpandProofReferencesAnalyst implements IProofReferencesA * {@inheritDoc} */ @Override - public LinkedHashSet> computeReferences(Node node, Services services) { - if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) { + public @Nullable LinkedHashSet> computeReferences(Node node, + Services services) { + if (node.getAppliedRuleApp() != null) { NodeInfo info = node.getNodeInfo(); if (info.getActiveStatement() instanceof MethodBodyStatement mbs) { IProgramMethod pm = mbs.getProgramMethod(services); diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java index 4e662a8cc48..a1a006be0b3 100644 --- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java @@ -33,6 +33,8 @@ import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.Nullable; + /** * Extracts called methods. * @@ -43,35 +45,32 @@ public class MethodCallProofReferencesAnalyst implements IProofReferencesAnalyst * {@inheritDoc} */ @Override - public LinkedHashSet> computeReferences(Node node, Services services) { + public @Nullable LinkedHashSet> computeReferences(Node node, + Services services) { String name = MiscTools.getRuleName(node); if (name != null && name.toLowerCase().contains("methodcall")) { NodeInfo info = node.getNodeInfo(); - if (info != null) { - if (info.getActiveStatement() instanceof MethodReference) { - ExecutionContext context = extractContext(node, services); - IProofReference reference = createReference(node, services, - context, (MethodReference) info.getActiveStatement()); - LinkedHashSet> result = - new LinkedHashSet<>(); - result.add(reference); - return result; - } else if (info.getActiveStatement() instanceof Assignment assignment) { - ExecutionContext context = extractContext(node, services); - LinkedHashSet> result = - new LinkedHashSet<>(); - for (int i = 0; i < assignment.getChildCount(); i++) { - ProgramElement child = assignment.getChildAt(i); - if (child instanceof MethodReference) { - IProofReference reference = - createReference(node, services, context, (MethodReference) child); - ProofReferenceUtil.merge(result, reference); - } + if (info.getActiveStatement() instanceof MethodReference) { + ExecutionContext context = extractContext(node, services); + IProofReference reference = createReference(node, services, + context, (MethodReference) info.getActiveStatement()); + LinkedHashSet> result = + new LinkedHashSet<>(); + result.add(reference); + return result; + } else if (info.getActiveStatement() instanceof Assignment assignment) { + ExecutionContext context = extractContext(node, services); + LinkedHashSet> result = + new LinkedHashSet<>(); + for (int i = 0; i < assignment.getChildCount(); i++) { + ProgramElement child = assignment.getChildAt(i); + if (child instanceof MethodReference) { + IProofReference reference = + createReference(node, services, context, (MethodReference) child); + ProofReferenceUtil.merge(result, reference); } - return result; - } else { - return null; } + return result; } else { return null; } diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java index 1d46d466ec9..f467b45e753 100644 --- a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java @@ -20,6 +20,8 @@ import de.uka.ilkd.key.proof_references.reference.DefaultProofReference; import de.uka.ilkd.key.proof_references.reference.IProofReference; +import org.jspecify.annotations.Nullable; + /** * Extracts read and write access to fields ({@link IProgramVariable}) via assignments. * @@ -30,8 +32,9 @@ public class ProgramVariableReferencesAnalyst implements IProofReferencesAnalyst * {@inheritDoc} */ @Override - public LinkedHashSet> computeReferences(Node node, Services services) { - if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) { + public @Nullable LinkedHashSet> computeReferences(Node node, + Services services) { + if (node.getAppliedRuleApp() != null) { SourceElement statement = node.getNodeInfo().getActiveStatement(); if (statement instanceof CopyAssignment) { LinkedHashSet> result = new LinkedHashSet<>(); diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/package-info.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/package-info.java new file mode 100644 index 00000000000..9a1f0be11be --- /dev/null +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (5/11/25) + */ +@NullMarked +package de.uka.ilkd.key.proof_references.analyst; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/package-info.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/package-info.java new file mode 100644 index 00000000000..e008ba07ef1 --- /dev/null +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (5/11/25) + */ +@NullMarked +package de.uka.ilkd.key.proof_references; + +import org.jspecify.annotations.NullMarked; 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..335f9f95460 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 @@ -12,6 +12,8 @@ import org.key_project.util.Strings; +import org.jspecify.annotations.Nullable; + /** * Default implementation of {@link IProofReference}. * @@ -26,7 +28,7 @@ public class DefaultProofReference implements IProofReference { /** * The source {@link Proof}. */ - private final Proof source; + private final @Nullable Proof source; /** * The target source member. @@ -45,7 +47,7 @@ public class DefaultProofReference implements IProofReference { * @param node Node to access the source {@link Proof} (or null). * @param target The target source member. */ - public DefaultProofReference(String kind, Node node, T target) { + public DefaultProofReference(String kind, @Nullable Node node, T target) { this.kind = kind; this.source = node != null ? node.proof() : null; this.target = target; @@ -88,7 +90,7 @@ public String getKind() { * {@inheritDoc} */ @Override - public Proof getSource() { + public @Nullable Proof getSource() { return source; } @@ -96,7 +98,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.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/package-info.java b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/package-info.java new file mode 100644 index 00000000000..0c4ce725ae2 --- /dev/null +++ b/key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (5/11/25) + */ +@NullMarked +package de.uka.ilkd.key.proof_references.reference; + +import org.jspecify.annotations.NullMarked; diff --git a/key.core.rifl/build.gradle b/key.core.rifl/build.gradle index 5d5aa84bf64..dd57511e462 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..081276069f3 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 @@ -11,6 +11,9 @@ import org.key_project.util.collection.KeYCollections; import org.key_project.util.collection.Pair; +import org.checkerframework.checker.nullness.qual.EnsuresNonNull; +import org.checkerframework.checker.nullness.qual.KeyFor; +import org.checkerframework.checker.nullness.qual.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; import org.xml.sax.Attributes; @@ -84,10 +87,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 @Nullable String tmpHandle = null; private String category = DEFAULT_CATEGORY; @@ -96,17 +99,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 +131,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 +143,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,7 +156,10 @@ 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"); @@ -196,6 +211,7 @@ private void checkDomainAssignmentsWithFlows() { */ } + @SuppressWarnings("nullness") private void checkFlows() { for (var p : categories2domains.entrySet()) { assert domains.contains(categories2domains.get(p.getKey())); @@ -203,7 +219,8 @@ 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 e0b52aee16f..4de64fa9b9f 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 @@ -120,7 +120,7 @@ public static Path getDefaultSavePath(Path origSourcePath) { private static Path getBaseDirPath(Path origSourcePath) { if (Files.isRegularFile(origSourcePath)) { - return origSourcePath.getParent(); + return Objects.requireNonNull(origSourcePath.getParent()); } 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.example/src/main/java/org/key_project/example/Main.java b/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java index 39f907c55f1..f7c4b3768a6 100644 --- a/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java +++ b/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java @@ -35,6 +35,7 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.java.StringUtil; +import org.jspecify.annotations.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -148,8 +149,8 @@ public static void main(String[] args) { * @param builder The {@link SymbolicExecutionTreeBuilder} providing the root of the symbolic * execution tree. */ - protected static void printSymbolicExecutionTree(String title, - SymbolicExecutionTreeBuilder builder) { + protected static void printSymbolicExecutionTree(@NonNull String title, + @NonNull SymbolicExecutionTreeBuilder builder) { System.out.println(title); System.out.println(StringUtil.repeat("=", title.length())); ExecutionNodePreorderIterator iterator = diff --git a/key.core.symbolic_execution.example/src/main/java/org/key_project/example/package-info.java b/key.core.symbolic_execution.example/src/main/java/org/key_project/example/package-info.java new file mode 100644 index 00000000000..9461c25ecce --- /dev/null +++ b/key.core.symbolic_execution.example/src/main/java/org/key_project/example/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package org.key_project.example; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/proof/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/proof/package-info.java new file mode 100644 index 00000000000..069d480873b --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/proof/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.proof; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/package-info.java new file mode 100644 index 00000000000..07ff312a57d --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.rule.label; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/strategy/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/strategy/package-info.java new file mode 100644 index 00000000000..4f36ce169ff --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/strategy/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.strategy; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractWriter.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractWriter.java index e519e28039f..eb2995c2776 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractWriter.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractWriter.java @@ -9,6 +9,9 @@ import org.key_project.util.java.StringUtil; import org.key_project.util.java.XMLUtil; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * Provides the basic functionality for classes like {@link ExecutionNodeWriter} and * {@link SymbolicLayoutWriter} which encodes an object structure as XML. @@ -49,8 +52,9 @@ public abstract class AbstractWriter { * @param attributeValues The attributes. * @param sb The {@link StringBuilder} to append to. */ - protected void appendEmptyTag(int level, String tagName, Map attributeValues, - StringBuilder sb) { + protected void appendEmptyTag(int level, @NonNull String tagName, + @NonNull Map attributeValues, + @NonNull StringBuilder sb) { XMLUtil.appendEmptyTag(level, tagName, attributeValues, sb); } @@ -62,8 +66,9 @@ protected void appendEmptyTag(int level, String tagName, Map att * @param attributeValues The attributes. * @param sb The {@link StringBuilder} to append to. */ - protected void appendStartTag(int level, String tagName, Map attributeValues, - StringBuilder sb) { + protected void appendStartTag(int level, String tagName, + @NonNull Map attributeValues, + @NonNull StringBuilder sb) { appendWhiteSpace(level, sb); sb.append("<"); sb.append(tagName); @@ -81,7 +86,7 @@ protected void appendStartTag(int level, String tagName, Map att * @param tagName The tag name. * @param sb The {@link StringBuilder} to append to. */ - protected void appendEndTag(int level, String tagName, StringBuilder sb) { + protected void appendEndTag(int level, String tagName, @NonNull StringBuilder sb) { appendWhiteSpace(level, sb); sb.append(""); @@ -134,7 +140,7 @@ protected void appendXmlHeader(String encoding, StringBuilder sb) { * * @param sb The {@link StringBuilder} to write to. */ - protected void appendNewLine(StringBuilder sb) { + protected void appendNewLine(@NonNull StringBuilder sb) { sb.append(NEW_LINE); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodePreorderIterator.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodePreorderIterator.java index ded295278ea..b011257b826 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodePreorderIterator.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodePreorderIterator.java @@ -5,6 +5,9 @@ import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** *

* Iterates preorder over the whole sub tree of a given {@link IExecutionNode}. @@ -85,7 +88,7 @@ protected void updateNext() { * @param node The visited {@link IExecutionNode}. * @return The next {@link IExecutionNode} to visit. */ - protected IExecutionNode getNextOnParent(IExecutionNode node) { + protected @Nullable IExecutionNode getNextOnParent(@NonNull IExecutionNode node) { IExecutionNode parent = node.getParent(); while (parent != null) { boolean IExecutionNodeFound = false; // Indicates that IExecutionNode was found on the diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeSymbolicLayoutExtractor.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeSymbolicLayoutExtractor.java index 4b6cb070107..bcd7127eae4 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeSymbolicLayoutExtractor.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeSymbolicLayoutExtractor.java @@ -7,6 +7,8 @@ import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; +import org.jspecify.annotations.NonNull; + /** * Special {@link SymbolicLayoutExtractor} for {@link IExecutionNode}s. * @@ -16,14 +18,14 @@ public class ExecutionNodeSymbolicLayoutExtractor extends SymbolicLayoutExtracto /** * The {@link IExecutionNode} to extract memory layouts from. */ - private final IExecutionNode executionNode; + private final @NonNull IExecutionNode executionNode; /** * Constructor. * * @param executionNode The {@link IExecutionNode} to extract memory layouts from. */ - public ExecutionNodeSymbolicLayoutExtractor(IExecutionNode executionNode) { + public ExecutionNodeSymbolicLayoutExtractor(@NonNull IExecutionNode executionNode) { super(executionNode.getProofNode(), executionNode.getModalityPIO(), executionNode.getSettings().useUnicode(), executionNode.getSettings().usePrettyPrinting(), diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeWriter.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeWriter.java index 33c282a19eb..561099c9de5 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeWriter.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeWriter.java @@ -40,6 +40,9 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.java.ArrayUtil; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * Allows to persistent selected properties of {@link IExecutionNode}s as XML file. Such files can * be read via an {@link ExecutionNodeReader} instance. @@ -364,7 +367,8 @@ public class ExecutionNodeWriter extends AbstractWriter { * @throws IOException Occurred Exception. * @throws ProofInputException Occurred Exception. */ - public void write(IExecutionNode node, String encoding, File file, boolean saveVariables, + public void write(IExecutionNode node, String encoding, @NonNull File file, + boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints) throws IOException, ProofInputException { try (var out = new FileOutputStream(file)) { @@ -387,7 +391,7 @@ public void write(IExecutionNode node, String encoding, File file, boolean sa * @throws IOException Occurred Exception. * @throws ProofInputException Occurred Exception. */ - public void write(IExecutionNode node, String encoding, OutputStream out, + public void write(IExecutionNode node, @Nullable String encoding, @Nullable OutputStream out, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints) throws IOException, ProofInputException { if (out != null) { @@ -411,7 +415,7 @@ public void write(IExecutionNode node, String encoding, OutputStream out, * @return The created XML content. * @throws ProofInputException Occurred Exception. */ - public String toXML(IExecutionNode node, String encoding, boolean saveVariables, + public @NonNull String toXML(IExecutionNode node, String encoding, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints) throws ProofInputException { StringBuilder sb = new StringBuilder(); @@ -436,7 +440,7 @@ public String toXML(IExecutionNode node, String encoding, boolean saveVariabl */ protected void appendExecutionNode(int level, IExecutionNode node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, - StringBuilder sb) throws ProofInputException { + @NonNull StringBuilder sb) throws ProofInputException { if (node instanceof IExecutionBranchCondition) { appendExecutionBranchCondition(level, (IExecutionBranchCondition) node, saveVariables, saveCallStack, saveReturnValues, saveConstraints, sb); @@ -497,9 +501,10 @@ protected void appendExecutionNode(int level, IExecutionNode node, boolean sa * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionBranchCondition(int level, IExecutionBranchCondition node, + protected void appendExecutionBranchCondition(int level, + @NonNull IExecutionBranchCondition node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -533,9 +538,10 @@ protected void appendExecutionBranchCondition(int level, IExecutionBranchConditi * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionStart(int level, IExecutionStart node, boolean saveVariables, + protected void appendExecutionStart(int level, @NonNull IExecutionStart node, + boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, - StringBuilder sb) throws ProofInputException { + @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -559,7 +565,8 @@ protected void appendExecutionStart(int level, IExecutionStart node, boolean sav * @param node The {@link IExecutionStart} which provides the termination entries. * @param sb The {@link StringBuilder} to append to. */ - protected void appendTerminations(int level, IExecutionStart node, StringBuilder sb) { + protected void appendTerminations(int level, @NonNull IExecutionStart node, + @NonNull StringBuilder sb) { ImmutableList terminations = node.getTerminations(); if (terminations != null) { for (IExecutionTermination termination : terminations) { @@ -583,9 +590,10 @@ protected void appendTerminations(int level, IExecutionStart node, StringBuilder * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionBranchStatement(int level, IExecutionBranchStatement node, + protected void appendExecutionBranchStatement(int level, + @NonNull IExecutionBranchStatement node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -616,9 +624,9 @@ protected void appendExecutionBranchStatement(int level, IExecutionBranchStateme * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionLoopCondition(int level, IExecutionLoopCondition node, + protected void appendExecutionLoopCondition(int level, @NonNull IExecutionLoopCondition node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -649,9 +657,9 @@ protected void appendExecutionLoopCondition(int level, IExecutionLoopCondition n * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionLoopStatement(int level, IExecutionLoopStatement node, + protected void appendExecutionLoopStatement(int level, @NonNull IExecutionLoopStatement node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -682,9 +690,9 @@ protected void appendExecutionLoopStatement(int level, IExecutionLoopStatement n * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionMethodCall(int level, IExecutionMethodCall node, + protected void appendExecutionMethodCall(int level, @NonNull IExecutionMethodCall node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -714,9 +722,9 @@ protected void appendExecutionMethodCall(int level, IExecutionMethodCall node, * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionMethodReturn(int level, IExecutionMethodReturn node, + protected void appendExecutionMethodReturn(int level, @NonNull IExecutionMethodReturn node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_SIGNATURE, node.getSignature()); @@ -763,8 +771,9 @@ protected void appendExecutionMethodReturn(int level, IExecutionMethodReturn nod * @throws ProofInputException Occurred Exception. */ protected void appendExecutionExceptionalMethodReturn(int level, - IExecutionExceptionalMethodReturn node, boolean saveVariables, boolean saveCallStack, - boolean saveReturnValues, boolean saveConstraints, StringBuilder sb) + @NonNull IExecutionExceptionalMethodReturn node, boolean saveVariables, + boolean saveCallStack, + boolean saveReturnValues, boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); @@ -795,7 +804,8 @@ protected void appendExecutionExceptionalMethodReturn(int level, * @throws ProofInputException Occurred Exception. */ protected void appendExecutionMethodReturnValue(int level, - IExecutionMethodReturnValue returnValue, StringBuilder sb) throws ProofInputException { + @NonNull IExecutionMethodReturnValue returnValue, @NonNull StringBuilder sb) + throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, returnValue.getName()); attributeValues.put(ATTRIBUTE_RETURN_VALUE_STRING, returnValue.getReturnValueString()); @@ -818,9 +828,9 @@ protected void appendExecutionMethodReturnValue(int level, * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionStatement(int level, IExecutionStatement node, + protected void appendExecutionStatement(int level, @NonNull IExecutionStatement node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -849,9 +859,10 @@ protected void appendExecutionStatement(int level, IExecutionStatement node, * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionJoin(int level, IExecutionJoin node, boolean saveVariables, + protected void appendExecutionJoin(int level, @NonNull IExecutionJoin node, + boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, - StringBuilder sb) throws ProofInputException { + @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -881,9 +892,10 @@ protected void appendExecutionJoin(int level, IExecutionJoin node, boolean saveV * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionOperationContract(int level, IExecutionOperationContract node, + protected void appendExecutionOperationContract(int level, + @NonNull IExecutionOperationContract node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -921,9 +933,9 @@ protected void appendExecutionOperationContract(int level, IExecutionOperationCo * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionLoopInvariant(int level, IExecutionLoopInvariant node, + protected void appendExecutionLoopInvariant(int level, @NonNull IExecutionLoopInvariant node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -955,9 +967,10 @@ protected void appendExecutionLoopInvariant(int level, IExecutionLoopInvariant n * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionBlockContract(int level, IExecutionAuxiliaryContract node, + protected void appendExecutionBlockContract(int level, + @NonNull IExecutionAuxiliaryContract node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -989,9 +1002,9 @@ protected void appendExecutionBlockContract(int level, IExecutionAuxiliaryContra * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendExecutionTermination(int level, IExecutionTermination node, + protected void appendExecutionTermination(int level, @NonNull IExecutionTermination node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, node.getName()); attributeValues.put(ATTRIBUTE_PATH_CONDITION, node.getFormatedPathCondition()); @@ -1018,8 +1031,9 @@ protected void appendExecutionTermination(int level, IExecutionTermination node, * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendConstraints(int level, IExecutionValue value, boolean saveConstraints, - StringBuilder sb) throws ProofInputException { + protected void appendConstraints(int level, @NonNull IExecutionValue value, + boolean saveConstraints, + @NonNull StringBuilder sb) throws ProofInputException { if (saveConstraints) { IExecutionConstraint[] constraints = value.getConstraints(); for (IExecutionConstraint constraint : constraints) { @@ -1037,8 +1051,9 @@ protected void appendConstraints(int level, IExecutionValue value, boolean saveC * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendConstraints(int level, IExecutionNode node, boolean saveConstraints, - StringBuilder sb) throws ProofInputException { + protected void appendConstraints(int level, @NonNull IExecutionNode node, + boolean saveConstraints, + @NonNull StringBuilder sb) throws ProofInputException { if (saveConstraints) { IExecutionConstraint[] constraints = node.getConstraints(); for (IExecutionConstraint constraint : constraints) { @@ -1056,7 +1071,8 @@ protected void appendConstraints(int level, IExecutionNode node, boolean save * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendConstraint(int level, IExecutionConstraint constraint, StringBuilder sb) + protected void appendConstraint(int level, @NonNull IExecutionConstraint constraint, + @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, constraint.getName()); @@ -1073,8 +1089,9 @@ protected void appendConstraint(int level, IExecutionConstraint constraint, Stri * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendVariables(int level, IExecutionNode node, boolean saveVariables, - boolean saveConstraints, StringBuilder sb) throws ProofInputException { + protected void appendVariables(int level, @NonNull IExecutionNode node, + boolean saveVariables, + boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { if (saveVariables) { IExecutionVariable[] variables = node.getVariables(); for (IExecutionVariable variable : variables) { @@ -1093,8 +1110,8 @@ protected void appendVariables(int level, IExecutionNode node, boolean saveVa * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendCallStateVariables(int level, IExecutionBaseMethodReturn node, - boolean saveVariables, boolean saveConstraints, StringBuilder sb) + protected void appendCallStateVariables(int level, @NonNull IExecutionBaseMethodReturn node, + boolean saveVariables, boolean saveConstraints, @NonNull StringBuilder sb) throws ProofInputException { if (saveVariables) { IExecutionVariable[] variables = node.getCallStateVariables(); @@ -1115,8 +1132,9 @@ protected void appendCallStateVariables(int level, IExecutionBaseMethodReturn * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendVariable(int level, IExecutionVariable variable, boolean saveConstraints, - String tagName, StringBuilder sb) throws ProofInputException { + protected void appendVariable(int level, @NonNull IExecutionVariable variable, + boolean saveConstraints, + String tagName, @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, variable.getName()); attributeValues.put(ATTRIBUTE_ARRAY_INDEX, variable.getArrayIndexString()); @@ -1135,8 +1153,9 @@ protected void appendVariable(int level, IExecutionVariable variable, boolean sa * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendValues(int level, IExecutionVariable variable, boolean saveConstraints, - StringBuilder sb) throws ProofInputException { + protected void appendValues(int level, @NonNull IExecutionVariable variable, + boolean saveConstraints, + @NonNull StringBuilder sb) throws ProofInputException { IExecutionValue[] values = variable.getValues(); for (IExecutionValue value : values) { appendValue(level, value, saveConstraints, sb); @@ -1153,8 +1172,8 @@ protected void appendValues(int level, IExecutionVariable variable, boolean save * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendValue(int level, IExecutionValue value, boolean saveConstraints, - StringBuilder sb) throws ProofInputException { + protected void appendValue(int level, @NonNull IExecutionValue value, boolean saveConstraints, + @NonNull StringBuilder sb) throws ProofInputException { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, value.getName()); attributeValues.put(ATTRIBUTE_TYPE_STRING, value.getTypeString()); @@ -1185,9 +1204,10 @@ protected void appendValue(int level, IExecutionValue value, boolean saveConstra * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception. */ - protected void appendChildren(int childLevel, IExecutionNode parent, boolean saveVariables, + protected void appendChildren(int childLevel, @NonNull IExecutionNode parent, + boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, - StringBuilder sb) throws ProofInputException { + @NonNull StringBuilder sb) throws ProofInputException { IExecutionNode[] children = parent.getChildren(); for (IExecutionNode child : children) { appendExecutionNode(childLevel, child, saveVariables, saveCallStack, saveReturnValues, @@ -1202,7 +1222,8 @@ protected void appendChildren(int childLevel, IExecutionNode parent, boolean * @param node the {@link IExecutionNode} whose outgoing links are to be reported * @param sb the StringBuilder with the resulting text description */ - protected void appendOutgoingLinks(int level, IExecutionNode node, StringBuilder sb) { + protected void appendOutgoingLinks(int level, @NonNull IExecutionNode node, + @NonNull StringBuilder sb) { if (!node.getOutgoingLinks().isEmpty()) { for (IExecutionLink link : node.getOutgoingLinks()) { appendOutgoingLink(level, link, sb); @@ -1217,7 +1238,8 @@ protected void appendOutgoingLinks(int level, IExecutionNode node, StringBuil * @param link the outgoing {@link IExecutionLink} to be reported * @param sb the StringBuilder with the resulting text description */ - protected void appendOutgoingLink(int level, IExecutionLink link, StringBuilder sb) { + protected void appendOutgoingLink(int level, @NonNull IExecutionLink link, + @NonNull StringBuilder sb) { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_PATH_IN_TREE, computePath(link.getTarget())); appendEmptyTag(level, TAG_OUTGOING_LINK, attributeValues, sb); @@ -1231,8 +1253,9 @@ protected void appendOutgoingLink(int level, IExecutionLink link, StringBuilder * @param saveCallStack Defines if the call stack should be saved or not. * @param sb The {@link StringBuilder} to append to. */ - protected void appendCallStack(int level, IExecutionNode node, boolean saveCallStack, - StringBuilder sb) { + protected void appendCallStack(int level, @NonNull IExecutionNode node, + boolean saveCallStack, + @NonNull StringBuilder sb) { if (saveCallStack) { IExecutionNode[] callStack = node.getCallStack(); if (callStack != null) { @@ -1252,7 +1275,8 @@ protected void appendCallStack(int level, IExecutionNode node, boolean saveCa * @param node The {@link IExecutionMethodCall} which provides the call stack. * @param sb The {@link StringBuilder} to append to. */ - protected void appendMethodReturns(int level, IExecutionMethodCall node, StringBuilder sb) { + protected void appendMethodReturns(int level, @NonNull IExecutionMethodCall node, + @NonNull StringBuilder sb) { ImmutableList> methodReturns = node.getMethodReturns(); if (methodReturns != null) { for (IExecutionBaseMethodReturn methodReturn : methodReturns) { @@ -1271,7 +1295,8 @@ protected void appendMethodReturns(int level, IExecutionMethodCall node, StringB * @param sb The {@link StringBuilder} to append to. * @throws ProofInputException Occurred Exception */ - protected void appendCompletedBlocks(int level, IExecutionNode node, StringBuilder sb) + protected void appendCompletedBlocks(int level, @NonNull IExecutionNode node, + @NonNull StringBuilder sb) throws ProofInputException { ImmutableList> completedBlocks = node.getCompletedBlocks(); if (completedBlocks != null) { @@ -1292,8 +1317,8 @@ protected void appendCompletedBlocks(int level, IExecutionNode node, StringBu * @param node The {@link IExecutionBlockStartNode} which provides the completed blocks. * @param sb The {@link StringBuilder} to append to. */ - protected void appendBlockCompletions(int level, IExecutionBlockStartNode node, - StringBuilder sb) { + protected void appendBlockCompletions(int level, @NonNull IExecutionBlockStartNode node, + @NonNull StringBuilder sb) { ImmutableList> blockCompletions = node.getBlockCompletions(); if (blockCompletions != null) { for (IExecutionNode blockCompletion : blockCompletions) { @@ -1311,7 +1336,7 @@ protected void appendBlockCompletions(int level, IExecutionBlockStartNode nod * @param node The {@link IExecutionNode} to compute path to. * @return The computed path. */ - protected String computePath(IExecutionNode node) { + protected @NonNull String computePath(@Nullable IExecutionNode node) { StringBuilder sb = new StringBuilder(); boolean afterFirst = false; while (node != null) { diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutWriter.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutWriter.java index 954b1dbc0dc..f24acef9d46 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutWriter.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutWriter.java @@ -19,6 +19,9 @@ import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicValue; import de.uka.ilkd.key.util.LinkedHashMap; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * Allows to persistent selected properties of {@link ISymbolicLayout}s as XML file. Such files can * be read via a {@link SymbolicLayoutReader} instance. @@ -125,7 +128,8 @@ public class SymbolicLayoutWriter extends AbstractWriter { * @param file The {@link File} to save to. * @throws IOException Occurred Exception. */ - public void write(ISymbolicLayout model, String encoding, File file) throws IOException { + public void write(@NonNull ISymbolicLayout model, String encoding, @NonNull File file) + throws IOException { write(model, encoding, new FileOutputStream(file)); } @@ -138,7 +142,8 @@ public void write(ISymbolicLayout model, String encoding, File file) throws IOEx * this method. * @throws IOException Occurred Exception. */ - public void write(ISymbolicLayout model, String encoding, OutputStream out) throws IOException { + public void write(@NonNull ISymbolicLayout model, @Nullable String encoding, + @Nullable OutputStream out) throws IOException { if (out != null) { try (out) { Charset charset = @@ -156,7 +161,7 @@ public void write(ISymbolicLayout model, String encoding, OutputStream out) thro * @param encoding The encoding to use. * @return The created XML content. */ - public String toXML(ISymbolicLayout model, String encoding) { + public @NonNull String toXML(@NonNull ISymbolicLayout model, String encoding) { StringBuilder sb = new StringBuilder(); appendXmlHeader(encoding, sb); appendModel(0, model, sb); @@ -171,7 +176,8 @@ public String toXML(ISymbolicLayout model, String encoding) { * @param model The {@link ISymbolicLayout} to append. * @param sb The {@link StringBuilder} to append to. */ - protected void appendModel(int level, ISymbolicLayout model, StringBuilder sb) { + protected void appendModel(int level, @NonNull ISymbolicLayout model, + @NonNull StringBuilder sb) { Map attributeValues = new LinkedHashMap<>(); appendStartTag(level, TAG_MODEL, attributeValues, sb); for (ISymbolicEquivalenceClass ec : model.getEquivalenceClasses()) { @@ -192,8 +198,8 @@ protected void appendModel(int level, ISymbolicLayout model, StringBuilder sb) { * @param ec The {@link ISymbolicEquivalenceClass} to append. * @param sb The {@link StringBuilder} to append to. */ - protected void appendEquivalenceClass(int level, ISymbolicEquivalenceClass ec, - StringBuilder sb) { + protected void appendEquivalenceClass(int level, @NonNull ISymbolicEquivalenceClass ec, + @NonNull StringBuilder sb) { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_REPRESENTATIVE, ec.getRepresentativeString()); appendStartTag(level, TAG_EQUIVALENCE_CLASS, attributeValues, sb); @@ -214,8 +220,9 @@ protected void appendEquivalenceClass(int level, ISymbolicEquivalenceClass ec, * @param state The {@link ISymbolicState} to append. * @param sb The {@link StringBuilder} to append to. */ - protected void appendState(int level, ISymbolicLayout model, ISymbolicState state, - StringBuilder sb) { + protected void appendState(int level, @NonNull ISymbolicLayout model, + @NonNull ISymbolicState state, + @NonNull StringBuilder sb) { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, state.getName()); appendStartTag(level, TAG_STATE, attributeValues, sb); @@ -237,8 +244,9 @@ protected void appendState(int level, ISymbolicLayout model, ISymbolicState stat * @param object The {@link ISymbolicObject} to append. * @param sb The {@link StringBuilder} to append to. */ - protected void appendObject(int level, ISymbolicLayout model, ISymbolicObject object, - StringBuilder sb) { + protected void appendObject(int level, @NonNull ISymbolicLayout model, + @NonNull ISymbolicObject object, + @NonNull StringBuilder sb) { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_XML_ID, computeObjectId(model, object)); attributeValues.put(ATTRIBUTE_NAME, object.getNameString()); @@ -261,7 +269,8 @@ protected void appendObject(int level, ISymbolicLayout model, ISymbolicObject ob * @param value The {@link ISymbolicValue} to append. * @param sb The {@link StringBuilder} to append to. */ - protected void appendValue(int level, ISymbolicValue value, StringBuilder sb) { + protected void appendValue(int level, @NonNull ISymbolicValue value, + @NonNull StringBuilder sb) { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, value.getName()); attributeValues.put(ATTRIBUTE_PROGRAM_VARIABLE, value.getProgramVariableString()); @@ -284,8 +293,8 @@ protected void appendValue(int level, ISymbolicValue value, StringBuilder sb) { * @param association The {@link ISymbolicAssociation} to append. * @param sb The {@link StringBuilder} to append to. */ - protected void appendAssociation(int level, ISymbolicLayout model, - ISymbolicAssociation association, StringBuilder sb) { + protected void appendAssociation(int level, @NonNull ISymbolicLayout model, + @NonNull ISymbolicAssociation association, @NonNull StringBuilder sb) { Map attributeValues = new LinkedHashMap<>(); attributeValues.put(ATTRIBUTE_NAME, association.getName()); attributeValues.put(ATTRIBUTE_PROGRAM_VARIABLE, association.getProgramVariableString()); @@ -305,7 +314,8 @@ protected void appendAssociation(int level, ISymbolicLayout model, * @param object The {@link ISymbolicObject} to compute its unique ID. * @return The unique ID. */ - protected String computeObjectId(ISymbolicLayout model, ISymbolicObject object) { + protected @NonNull String computeObjectId(@NonNull ISymbolicLayout model, + ISymbolicObject object) { int i = 0; int index = -1; Iterator iter = model.getObjects().iterator(); diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionAuxiliaryContract.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionAuxiliaryContract.java index 7b2e2f27990..5cfa54f628f 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionAuxiliaryContract.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionAuxiliaryContract.java @@ -10,6 +10,8 @@ import de.uka.ilkd.key.symbolic_execution.SymbolicExecutionTreeBuilder; import de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionAuxiliaryContract; +import org.jspecify.annotations.Nullable; + /** *

* A node in the symbolic execution tree which represents a use block/loop contract application. @@ -29,6 +31,7 @@ public interface IExecutionAuxiliaryContract extends IExecutionNode * A node in the symbolic execution tree which represents a loop condition, e.g. {@code x >= 0}. @@ -28,6 +30,7 @@ public interface IExecutionLoopCondition extends IExecutionBlockStartNode * A node in the symbolic execution tree which represents a loop invariant application. @@ -28,6 +30,7 @@ public interface IExecutionLoopInvariant extends IExecutionNode { * * @return The used {@link LoopSpecification}. */ + @Nullable LoopSpecification getLoopInvariant(); /** @@ -35,6 +38,7 @@ public interface IExecutionLoopInvariant extends IExecutionNode { * * @return The loop statement which is simulated by its loop invariant. */ + @Nullable While getLoopStatement(); /** diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionMethodCall.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionMethodCall.java index d36b33bb802..fc5cb2f14f0 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionMethodCall.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionMethodCall.java @@ -11,6 +11,8 @@ import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; + /** *

* A node in the symbolic execution tree which represents a method call, e.g. {@code foo()}. @@ -30,6 +32,7 @@ public interface IExecutionMethodCall extends IExecutionNode * A node in the symbolic execution tree which represents the normal termination of a branch, e.g. @@ -46,6 +48,7 @@ public interface IExecutionTermination extends IExecutionNode { * * @return The {@link IProgramVariable} which is used to caught global exceptions. */ + @Nullable IProgramVariable getExceptionVariable(); /** @@ -53,6 +56,7 @@ public interface IExecutionTermination extends IExecutionNode { * * @return The {@link Sort} of the caught exception. */ + @Nullable Sort getExceptionSort(); /** diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/AbstractExecutionBlockStartNode.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/AbstractExecutionBlockStartNode.java index 1df213ab4c9..683711c8f80 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/AbstractExecutionBlockStartNode.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/AbstractExecutionBlockStartNode.java @@ -12,6 +12,9 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * Provides a basic implementation of {@link IExecutionBlockStartNode}. * @@ -22,7 +25,7 @@ public abstract class AbstractExecutionBlockStartNode /** * The up to know discovered completing {@link IExecutionNode}s. */ - private ImmutableList> blockCompletions = ImmutableSLList.nil(); + private @NonNull ImmutableList> blockCompletions = ImmutableSLList.nil(); /** * Defines if a block is or might be opened. @@ -81,7 +84,7 @@ public void removeBlockCompletion(IExecutionNode completion) { * * @param blockCompletion The {@link IExecutionNode} to register. */ - public void addBlockCompletion(IExecutionNode blockCompletion) { + public void addBlockCompletion(@Nullable IExecutionNode blockCompletion) { if (blockCompletion != null && !blockCompletions.contains(blockCompletion)) { if (blockCompletion instanceof AbstractExecutionNode) { blockCompletions = blockCompletions.append(blockCompletion); diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionBranchStatement.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionBranchStatement.java index dc97d520667..7868c5fe0c4 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionBranchStatement.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionBranchStatement.java @@ -14,6 +14,8 @@ import de.uka.ilkd.key.symbolic_execution.model.ITreeSettings; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; +import org.jspecify.annotations.NonNull; + /** * The default implementation of {@link IExecutionBranchStatement}. * @@ -36,7 +38,7 @@ public ExecutionBranchStatement(ITreeSettings settings, Node proofNode) { * {@inheritDoc} */ @Override - protected String lazyComputeName() { + protected @NonNull String lazyComputeName() { BranchStatement bs = getActiveStatement(); if (bs instanceof If) { PrettyPrinter p = PrettyPrinter.purePrinter(); @@ -55,7 +57,7 @@ protected String lazyComputeName() { * {@inheritDoc} */ @Override - protected IExecutionConstraint[] lazyComputeConstraints() { + protected IExecutionConstraint @NonNull [] lazyComputeConstraints() { return SymbolicExecutionUtil.createExecutionConstraints(this); } @@ -63,7 +65,7 @@ protected IExecutionConstraint[] lazyComputeConstraints() { * {@inheritDoc} */ @Override - public String getElementType() { + public @NonNull String getElementType() { return "Branch Statement"; } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionExceptionalMethodReturn.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionExceptionalMethodReturn.java index ae9dbaa77f5..763f316cd9a 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionExceptionalMethodReturn.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionExceptionalMethodReturn.java @@ -18,6 +18,8 @@ import org.key_project.util.java.StringUtil; +import org.jspecify.annotations.NonNull; + /** * The default implementation of {@link IExecutionExceptionalMethodReturn}. * @@ -34,7 +36,7 @@ public class ExecutionExceptionalMethodReturn extends AbstractExecutionMethodRet * @param methodCall The {@link IExecutionMethodCall} which is now returned. */ public ExecutionExceptionalMethodReturn(ITreeSettings settings, Node proofNode, - ExecutionMethodCall methodCall) { + @NonNull ExecutionMethodCall methodCall) { super(settings, proofNode, methodCall); } @@ -42,7 +44,7 @@ public ExecutionExceptionalMethodReturn(ITreeSettings settings, Node proofNode, * {@inheritDoc} */ @Override - protected String lazyComputeName() { + protected @NonNull String lazyComputeName() { String exceptionType; Expression expression = getActiveStatement().getExpression(); if (expression instanceof ProgramVariable) { @@ -58,7 +60,7 @@ protected String lazyComputeName() { * {@inheritDoc} */ @Override - protected IExecutionConstraint[] lazyComputeConstraints() { + protected IExecutionConstraint @NonNull [] lazyComputeConstraints() { return SymbolicExecutionUtil.createExecutionConstraints(this); } @@ -66,7 +68,7 @@ protected IExecutionConstraint[] lazyComputeConstraints() { * {@inheritDoc} */ @Override - protected String lazyComputeSignature() throws ProofInputException { + protected @NonNull String lazyComputeSignature() throws ProofInputException { String methodName = getMethodCall().getName(); return INTERNAL_NODE_NAME_START + "exceptional return" + (!StringUtil.isTrimmedEmpty(methodName) ? " of " + methodName : "") @@ -77,7 +79,7 @@ protected String lazyComputeSignature() throws ProofInputException { * {@inheritDoc} */ @Override - public String getElementType() { + public @NonNull String getElementType() { return "Exceptional Method Return"; } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionJoin.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionJoin.java index fa81adcf2ca..a612cec684b 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionJoin.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionJoin.java @@ -11,6 +11,8 @@ import de.uka.ilkd.key.symbolic_execution.model.ITreeSettings; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; +import org.jspecify.annotations.NonNull; + /** * The default implementation of {@link IExecutionJoin}. * @@ -24,7 +26,7 @@ public class ExecutionJoin extends AbstractExecutionNode implemen * @param proofNode The {@link Node} of KeY's proof tree which is represented by this * {@link IExecutionNode}. */ - public ExecutionJoin(ITreeSettings settings, Node proofNode) { + public ExecutionJoin(@NonNull ITreeSettings settings, @NonNull Node proofNode) { super(settings, proofNode); } @@ -32,7 +34,7 @@ public ExecutionJoin(ITreeSettings settings, Node proofNode) { * {@inheritDoc} */ @Override - protected String lazyComputeName() { + protected @NonNull String lazyComputeName() { return "Join"; } @@ -40,7 +42,7 @@ protected String lazyComputeName() { * {@inheritDoc} */ @Override - protected IExecutionConstraint[] lazyComputeConstraints() { + protected IExecutionConstraint @NonNull [] lazyComputeConstraints() { return SymbolicExecutionUtil.createExecutionConstraints(this); } @@ -48,7 +50,7 @@ protected IExecutionConstraint[] lazyComputeConstraints() { * {@inheritDoc} */ @Override - public String getElementType() { + public @NonNull String getElementType() { return "Join"; } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopCondition.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopCondition.java index b0eb7159950..ee339af25a5 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopCondition.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopCondition.java @@ -15,6 +15,9 @@ import de.uka.ilkd.key.symbolic_execution.model.ITreeSettings; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * The default implementation of {@link IExecutionLoopCondition}. * @@ -45,7 +48,7 @@ protected String lazyComputeName() { * {@inheritDoc} */ @Override - public Expression getGuardExpression() { + public @Nullable Expression getGuardExpression() { if (getActiveStatement() instanceof LoopStatement) { return ((LoopStatement) getActiveStatement()).getGuardExpression(); } else if (getActiveStatement() instanceof If) { @@ -59,7 +62,7 @@ public Expression getGuardExpression() { * {@inheritDoc} */ @Override - public PositionInfo getGuardExpressionPositionInfo() { + public @NonNull PositionInfo getGuardExpressionPositionInfo() { return getGuardExpression().getPositionInfo(); } @@ -67,7 +70,7 @@ public PositionInfo getGuardExpressionPositionInfo() { * {@inheritDoc} */ @Override - protected IExecutionConstraint[] lazyComputeConstraints() { + protected IExecutionConstraint @NonNull [] lazyComputeConstraints() { return SymbolicExecutionUtil.createExecutionConstraints(this); } @@ -75,7 +78,7 @@ protected IExecutionConstraint[] lazyComputeConstraints() { * {@inheritDoc} */ @Override - public String getElementType() { + public @NonNull String getElementType() { return "Loop Condition"; } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopInvariant.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopInvariant.java index 3a10756d56e..f5a23dc545e 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopInvariant.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopInvariant.java @@ -14,6 +14,8 @@ import de.uka.ilkd.key.symbolic_execution.model.ITreeSettings; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; +import org.jspecify.annotations.NonNull; + /** * The default implementation of {@link IExecutionLoopInvariant}. * @@ -28,7 +30,7 @@ public class ExecutionLoopInvariant extends AbstractExecutionNode * @param proofNode The {@link Node} of KeY's proof tree which is represented by this * {@link IExecutionNode}. */ - public ExecutionLoopInvariant(ITreeSettings settings, Node proofNode) { + public ExecutionLoopInvariant(@NonNull ITreeSettings settings, @NonNull Node proofNode) { super(settings, proofNode); } @@ -44,7 +46,7 @@ public LoopInvariantBuiltInRuleApp getAppliedRuleApp() { * {@inheritDoc} */ @Override - protected String lazyComputeName() { + protected @NonNull String lazyComputeName() { return getLoopInvariant().getPlainText(getServices(), getAppliedRuleApp().getHeapContext(), getSettings().usePrettyPrinting(), getSettings().useUnicode()).trim(); } @@ -53,7 +55,7 @@ protected String lazyComputeName() { * {@inheritDoc} */ @Override - public String getElementType() { + public @NonNull String getElementType() { return "Loop Invariant"; } @@ -61,7 +63,7 @@ public String getElementType() { * {@inheritDoc} */ @Override - protected IExecutionConstraint[] lazyComputeConstraints() { + protected IExecutionConstraint @NonNull [] lazyComputeConstraints() { return SymbolicExecutionUtil.createExecutionConstraints(this); } @@ -69,7 +71,7 @@ protected IExecutionConstraint[] lazyComputeConstraints() { * {@inheritDoc} */ @Override - public LoopSpecification getLoopInvariant() { + public @NonNull LoopSpecification getLoopInvariant() { return ((LoopInvariantBuiltInRuleApp) getProofNode().getAppliedRuleApp()).getSpec(); } @@ -77,7 +79,7 @@ public LoopSpecification getLoopInvariant() { * {@inheritDoc} */ @Override - public While getLoopStatement() { + public @NonNull While getLoopStatement() { return ((LoopInvariantBuiltInRuleApp) getProofNode().getAppliedRuleApp()) .getLoopStatement(); } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopStatement.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopStatement.java index ba6acfee777..b3aef834375 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopStatement.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopStatement.java @@ -12,6 +12,8 @@ import de.uka.ilkd.key.symbolic_execution.model.ITreeSettings; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; +import org.jspecify.annotations.NonNull; + /** * The default implementation of {@link IExecutionLoopStatement}. * @@ -34,7 +36,7 @@ public ExecutionLoopStatement(ITreeSettings settings, Node proofNode) { * {@inheritDoc} */ @Override - protected String lazyComputeName() { + protected @NonNull String lazyComputeName() { LoopStatement ls = getActiveStatement(); if (ls.getGuardExpression() != null) { if (ls instanceof While) { @@ -65,7 +67,7 @@ protected String lazyComputeName() { * {@inheritDoc} */ @Override - protected IExecutionConstraint[] lazyComputeConstraints() { + protected IExecutionConstraint @NonNull [] lazyComputeConstraints() { return SymbolicExecutionUtil.createExecutionConstraints(this); } @@ -73,7 +75,7 @@ protected IExecutionConstraint[] lazyComputeConstraints() { * {@inheritDoc} */ @Override - public String getElementType() { + public @NonNull String getElementType() { return "Loop Statement"; } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionMethodCall.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionMethodCall.java index a5f0add941e..91f7b7082a2 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionMethodCall.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionMethodCall.java @@ -18,6 +18,9 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * The default implementation of {@link IExecutionMethodCall}. * @@ -28,7 +31,8 @@ public class ExecutionMethodCall extends AbstractExecutionNode> methodReturns = ImmutableSLList.nil(); + private @NonNull ImmutableList> methodReturns = + ImmutableSLList.nil(); /** * Constructor. @@ -37,7 +41,7 @@ public class ExecutionMethodCall extends AbstractExecutionNode> getMethodReturns() { * * @param methodReturn The {@link IExecutionBaseMethodReturn} to register. */ - public void addMethodReturn(IExecutionBaseMethodReturn methodReturn) { + public void addMethodReturn(@Nullable IExecutionBaseMethodReturn methodReturn) { if (methodReturn != null) { assert methodReturn.getMethodCall() == this; methodReturns = methodReturns.append(methodReturn); @@ -162,7 +166,7 @@ public void addMethodReturn(IExecutionBaseMethodReturn methodReturn) { * {@inheritDoc} */ @Override - protected IExecutionConstraint[] lazyComputeConstraints() { + protected IExecutionConstraint @NonNull [] lazyComputeConstraints() { return SymbolicExecutionUtil.createExecutionConstraints(this); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionMethodReturn.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionMethodReturn.java index 11427beb443..67fd8abca34 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionMethodReturn.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionMethodReturn.java @@ -40,6 +40,9 @@ import org.key_project.prover.engine.impl.ApplyStrategyInfo; import org.key_project.util.java.StringUtil; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * The default implementation of {@link IExecutionMethodReturn}. * @@ -71,7 +74,7 @@ public class ExecutionMethodReturn extends AbstractExecutionMethodReturn * @param proofNode The {@link Node} of KeY's proof tree which is represented by this * {@link IExecutionNode}. */ - public ExecutionStatement(ITreeSettings settings, Node proofNode) { + public ExecutionStatement(@NonNull ITreeSettings settings, @NonNull Node proofNode) { super(settings, proofNode); } @@ -41,7 +43,7 @@ protected String lazyComputeName() { * {@inheritDoc} */ @Override - protected IExecutionConstraint[] lazyComputeConstraints() { + protected IExecutionConstraint @NonNull [] lazyComputeConstraints() { return SymbolicExecutionUtil.createExecutionConstraints(this); } @@ -49,7 +51,7 @@ protected IExecutionConstraint[] lazyComputeConstraints() { * {@inheritDoc} */ @Override - public String getElementType() { + public @NonNull String getElementType() { return "Statement"; } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionTermination.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionTermination.java index 92114afa8a2..766bd427a52 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionTermination.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionTermination.java @@ -15,6 +15,9 @@ import org.key_project.logic.sort.Sort; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * The default implementation of {@link IExecutionTermination}. * @@ -31,7 +34,7 @@ public class ExecutionTermination extends AbstractExecutionNode /** * The {@link Sort} of the uncaught exception. */ - private Sort exceptionSort; + private @Nullable Sort exceptionSort; /** * The {@link TerminationKind}. @@ -49,7 +52,7 @@ public class ExecutionTermination extends AbstractExecutionNode * @param terminationKind The {@link TerminationKind} or {@code null} to compute it when it is * requested the first time (normal or exceptional termination only). */ - public ExecutionTermination(ITreeSettings settings, Node proofNode, + public ExecutionTermination(@NonNull ITreeSettings settings, @NonNull Node proofNode, IProgramVariable exceptionVariable, TerminationKind terminationKind) { super(settings, proofNode); this.exceptionVariable = exceptionVariable; @@ -60,7 +63,7 @@ public ExecutionTermination(ITreeSettings settings, Node proofNode, * {@inheritDoc} */ @Override - protected String lazyComputeName() { + protected @NonNull String lazyComputeName() { return switch (getTerminationKind()) { case EXCEPTIONAL -> INTERNAL_NODE_NAME_START + "uncaught " + exceptionSort + INTERNAL_NODE_NAME_END; @@ -86,7 +89,7 @@ public IProgramVariable getExceptionVariable() { * {@inheritDoc} */ @Override - public TerminationKind getTerminationKind() { + public @NonNull TerminationKind getTerminationKind() { if (terminationKind == null) { if (isBlockContractTermination()) { terminationKind = @@ -135,7 +138,7 @@ public Sort getExceptionSort() { * {@inheritDoc} */ @Override - protected IExecutionConstraint[] lazyComputeConstraints() { + protected IExecutionConstraint @NonNull [] lazyComputeConstraints() { return SymbolicExecutionUtil.createExecutionConstraints(this); } @@ -143,7 +146,7 @@ protected IExecutionConstraint[] lazyComputeConstraints() { * {@inheritDoc} */ @Override - public String getElementType() { + public @NonNull String getElementType() { return switch (getTerminationKind()) { case EXCEPTIONAL -> "Exceptional Termination"; case LOOP_BODY -> "Loop Body Termination"; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/package-info.java new file mode 100644 index 00000000000..d7cd054dd5b --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.model.impl; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/package-info.java new file mode 100644 index 00000000000..cb980230988 --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.model; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/ISymbolicAssociationValueContainer.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/ISymbolicAssociationValueContainer.java index 412fbf2db41..e2985a61d51 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/ISymbolicAssociationValueContainer.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/ISymbolicAssociationValueContainer.java @@ -9,6 +9,8 @@ import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; + /** *

* This interface is not instantiated directly because it defines only the common behavior of @@ -43,6 +45,7 @@ public interface ISymbolicAssociationValueContainer extends ISymbolicElement { * @return The found {@link ISymbolicAssociation} or {@code null} if no * {@link ISymbolicAssociation} is available with the given {@link IProgramVariable}. */ + @Nullable ISymbolicAssociation getAssociation(IProgramVariable programVariable, boolean isArrayIndex, JTerm arrayIndex, JTerm condition); @@ -64,6 +67,7 @@ ISymbolicAssociation getAssociation(IProgramVariable programVariable, * @return The found {@link ISymbolicValue} or {@code null} if no {@link ISymbolicValue} is * available with the given {@link IProgramVariable}. */ + @Nullable ISymbolicValue getValue(IProgramVariable programVariable, boolean isArrayIndex, JTerm arrayIndex, JTerm condition); } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/ISymbolicElement.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/ISymbolicElement.java index d81761b15f3..faf72f26d84 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/ISymbolicElement.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/ISymbolicElement.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.symbolic_execution.object_model; +import org.jspecify.annotations.Nullable; + /** * Defines the basic methods and properties each element in an symbolic object model has to have. * @@ -14,5 +16,6 @@ public interface ISymbolicElement { * * @return The {@link IModelSettings} to use. */ + @Nullable IModelSettings getSettings(); } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/SymbolicLayout.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/SymbolicLayout.java index fb2181fb47d..591fe93a4c6 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/SymbolicLayout.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/SymbolicLayout.java @@ -12,6 +12,8 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.NonNull; + /** * Default implementation of {@link ISymbolicLayout}. * @@ -21,7 +23,7 @@ public class SymbolicLayout extends AbstractElement implements ISymbolicLayout { /** * The contained {@link ISymbolicEquivalenceClass}. */ - private final ImmutableList equivalenceClasses; + private final @NonNull ImmutableList equivalenceClasses; /** * The {@link ISymbolicState}. @@ -31,7 +33,7 @@ public class SymbolicLayout extends AbstractElement implements ISymbolicLayout { /** * The contained {@link ISymbolicObject}s. */ - private ImmutableList objects = ImmutableSLList.nil(); + private @NonNull ImmutableList objects = ImmutableSLList.nil(); /** * Constructor. @@ -40,7 +42,7 @@ public class SymbolicLayout extends AbstractElement implements ISymbolicLayout { * @param settings The {@link IModelSettings} to use. */ public SymbolicLayout(IModelSettings settings, - ImmutableList equivalenceClasses) { + @NonNull ImmutableList equivalenceClasses) { super(settings); assert equivalenceClasses != null; this.equivalenceClasses = equivalenceClasses; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/SymbolicObject.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/SymbolicObject.java index 7113f3818eb..28c9d44fecb 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/SymbolicObject.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/SymbolicObject.java @@ -10,6 +10,9 @@ import org.key_project.logic.sort.Sort; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * Default implementation of {@link ISymbolicObject}. * @@ -60,7 +63,7 @@ public String getNameString() { * {@inheritDoc} */ @Override - public Sort getType() { + public @Nullable Sort getType() { return name != null ? name.sort() : null; } @@ -68,7 +71,7 @@ public Sort getType() { * {@inheritDoc} */ @Override - public String getTypeString() { + public @Nullable String getTypeString() { Sort sort = getType(); return sort != null ? sort.toString() : null; } @@ -77,7 +80,7 @@ public String getTypeString() { * {@inheritDoc} */ @Override - public String toString() { + public @NonNull String toString() { return "Object " + getNameString(); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/package-info.java new file mode 100644 index 00000000000..df118c56e41 --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.object_model.impl; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/package-info.java new file mode 100644 index 00000000000..20fe4430720 --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.object_model; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/package-info.java new file mode 100644 index 00000000000..fb45c1aaed4 --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/package-info.java new file mode 100644 index 00000000000..4d6f87d0c11 --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.po; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SimplifyTermProfile.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SimplifyTermProfile.java index fbce3ecb847..8fb2d7f0d37 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SimplifyTermProfile.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SimplifyTermProfile.java @@ -20,6 +20,8 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; +import org.jspecify.annotations.NonNull; + /** * An extended {@link JavaProfile} used in side proofs to simplify a {@link JTerm}. * @@ -58,7 +60,7 @@ public SimplifyTermProfile() { * {@inheritDoc} */ @Override - protected ImmutableList computeTermLabelConfiguration() { + protected @NonNull ImmutableList computeTermLabelConfiguration() { ImmutableList result = super.computeTermLabelConfiguration(); ImmutableList symExcPolicies = ImmutableSLList.nil() @@ -75,7 +77,7 @@ protected ImmutableList computeTermLabelConfiguration() * {@inheritDoc} */ @Override - protected ImmutableSet getStrategyFactories() { + protected @NonNull ImmutableSet getStrategyFactories() { return DefaultImmutableSet.nil().add(SIDE_PROOF_FACTORY); } @@ -83,7 +85,7 @@ protected ImmutableSet getStrategyFactories() { * {@inheritDoc} */ @Override - public StrategyFactory getDefaultStrategyFactory() { + public @NonNull StrategyFactory getDefaultStrategyFactory() { return SIDE_PROOF_FACTORY; } @@ -91,7 +93,7 @@ public StrategyFactory getDefaultStrategyFactory() { * {@inheritDoc} */ @Override - public String name() { + public @NonNull String name() { return NAME; } @@ -107,7 +109,7 @@ public String name() { * * @return The default instance for usage in the {@link Thread} of the user interface. */ - public static synchronized SimplifyTermProfile getDefaultInstance() { + public static synchronized @NonNull SimplifyTermProfile getDefaultInstance() { if (defaultInstance == null) { defaultInstance = new SimplifyTermProfile(); } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java index 4ab02a16076..cf5f63d3d4e 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java @@ -44,6 +44,9 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * An extended {@link JavaProfile} used by the symbolic execution API. * @@ -65,7 +68,7 @@ public class SymbolicExecutionJavaProfile extends JavaProfile { * {@code true} truth value evaluation is enabled, {@code false} truth value evaluation is * disabled. */ - private final Boolean truthValueEvaluationEnabled; + private final @NonNull Boolean truthValueEvaluationEnabled; /** *

@@ -106,7 +109,7 @@ public SymbolicExecutionJavaProfile(boolean predicateEvaluationEnabled) { * {@inheritDoc} */ @Override - protected ImmutableSet> computeSupportedGoalChooserBuilder() { + protected @NonNull ImmutableSet> computeSupportedGoalChooserBuilder() { return super.computeSupportedGoalChooserBuilder() .add(new SymbolicExecutionGoalChooserFactory()); } @@ -126,7 +129,7 @@ protected void initTermLabelManager() { * {@inheritDoc} */ @Override - protected ImmutableList computeTermLabelConfiguration() { + protected @NonNull ImmutableList computeTermLabelConfiguration() { ImmutableList result = super.computeTermLabelConfiguration(); result = result .prepend(getSymbolicExecutionTermLabelConfigurations(truthValueEvaluationEnabled)); @@ -140,7 +143,7 @@ protected ImmutableList computeTermLabelConfiguration() * predicate evaluation is disabled. * @return The additional {@link TermLabelFactory} instances used for symbolic execution. */ - public static ImmutableList getSymbolicExecutionTermLabelConfigurations( + public static @NonNull ImmutableList getSymbolicExecutionTermLabelConfigurations( boolean predicateEvaluationEnabled) { ImmutableList symExcPolicies = ImmutableSLList.nil().prepend(new StayOnOperatorTermLabelPolicy()); @@ -201,7 +204,7 @@ public static ImmutableList getSymbolicExecutionTermLabe * {@inheritDoc} */ @Override - protected ImmutableSet getStrategyFactories() { + protected @NonNull ImmutableSet getStrategyFactories() { ImmutableSet set = super.getStrategyFactories(); set = set.add(SYMBOLIC_EXECUTION_FACTORY); return set; @@ -211,7 +214,7 @@ protected ImmutableSet getStrategyFactories() { * {@inheritDoc} */ @Override - protected ImmutableList initBuiltInRules() { + protected @NonNull ImmutableList initBuiltInRules() { ImmutableList builtInRules = super.initBuiltInRules(); builtInRules = builtInRules.prepend(QuerySideProofRule.INSTANCE); builtInRules = builtInRules.prepend(ModalitySideProofRule.INSTANCE); @@ -222,7 +225,7 @@ protected ImmutableList initBuiltInRules() { * {@inheritDoc} */ @Override - public String name() { + public @NonNull String name() { return NAME; } @@ -266,7 +269,7 @@ public static synchronized SymbolicExecutionJavaProfile getDefaultInstance() { * {@code false} truth value evaluation is disabled. * @return The default instance for usage in the {@link Thread} of the user interface. */ - public static synchronized SymbolicExecutionJavaProfile getDefaultInstance( + public static synchronized @NonNull SymbolicExecutionJavaProfile getDefaultInstance( boolean truthValueEvaluationEnabled) { if (!truthValueEvaluationEnabled) { if (defaultInstance == null) { @@ -288,7 +291,7 @@ public static synchronized SymbolicExecutionJavaProfile getDefaultInstance( * @return {@code true} truth value evaluation is enabled, {@code false} truth value evaluation * is disabled. */ - public static boolean isTruthValueTracingEnabled(Proof proof) { + public static boolean isTruthValueTracingEnabled(@Nullable Proof proof) { if (proof != null && !proof.isDisposed()) { return isTruthValueEvaluationEnabled(proof.getInitConfig()); } else { @@ -303,7 +306,7 @@ public static boolean isTruthValueTracingEnabled(Proof proof) { * @return {@code true} truth value evaluation is enabled, {@code false} truth value evaluation * is disabled. */ - public static boolean isTruthValueEvaluationEnabled(InitConfig initConfig) { + public static boolean isTruthValueEvaluationEnabled(@Nullable InitConfig initConfig) { if (initConfig != null) { return isTruthValueEvaluationEnabled(initConfig.getProfile()); } else { diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfileDefaultProfileResolver.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfileDefaultProfileResolver.java index 0540ea16ab5..6404c4355bc 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfileDefaultProfileResolver.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfileDefaultProfileResolver.java @@ -6,6 +6,8 @@ import de.uka.ilkd.key.proof.init.DefaultProfileResolver; import de.uka.ilkd.key.proof.init.Profile; +import org.jspecify.annotations.NonNull; + /** * A {@link DefaultProfileResolver} which returns * {@link SymbolicExecutionJavaProfile#getDefaultInstance()}. @@ -17,7 +19,7 @@ public class SymbolicExecutionJavaProfileDefaultProfileResolver implements Defau * {@inheritDoc} */ @Override - public String getProfileName() { + public @NonNull String getProfileName() { return SymbolicExecutionJavaProfile.NAME; } @@ -25,7 +27,7 @@ public String getProfileName() { * {@inheritDoc} */ @Override - public Profile getDefaultProfile() { + public @NonNull Profile getDefaultProfile() { return SymbolicExecutionJavaProfile.getDefaultInstance(); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/package-info.java new file mode 100644 index 00000000000..dcd51cc1b82 --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.profile; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java index 17ad88fed2f..67e66f58328 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java @@ -119,7 +119,7 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) { * {@inheritDoc} */ @Override - public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { + public @NonNull IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { return new DefaultBuiltInRuleApp(this, pos); } @@ -225,7 +225,7 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { * {@inheritDoc} */ @Override - public Name name() { + public @NonNull Name name() { return NAME; } @@ -233,7 +233,7 @@ public Name name() { * {@inheritDoc} */ @Override - public String displayName() { + public @NonNull String displayName() { return NAME.toString(); } @@ -241,7 +241,7 @@ public String displayName() { * {@inheritDoc} */ @Override - public String toString() { + public @NonNull String toString() { return displayName(); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/package-info.java new file mode 100644 index 00000000000..7870de5ed45 --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.rule; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java index bfb10ac3e91..e00a3919c43 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java @@ -27,6 +27,8 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.NonNull; + /** * Provides a basic implementation of backward slicing algorithms. * @@ -37,7 +39,8 @@ public abstract class AbstractBackwardSlicer extends AbstractSlicer { * {@inheritDoc} */ @Override - public ImmutableArray doSlicing(Node seedNode, Location seedLocation, + public @NonNull ImmutableArray doSlicing(@NonNull Node seedNode, + @NonNull Location seedLocation, ImmutableList sec) throws ProofInputException { final Services services = seedNode.proof().getServices(); Set relevantLocations = null; @@ -113,7 +116,7 @@ protected abstract boolean accept(Node node, Node previousChild, Services servic * @param services The {@link Services} to use. */ protected void updateRelevantLocations(final ProgramElement read, - final Set relevantLocations, final SequentInfo info, + final @NonNull Set relevantLocations, final @NonNull SequentInfo info, final Services services) { ReferencePrefix relevantElement = toReferencePrefix(read); if (relevantElement != null) { @@ -139,9 +142,10 @@ protected void updateRelevantLocations(final ProgramElement read, * ({@link ThisReference}). * @return The updated locations. */ - protected Set updateOutdatedLocations(Services services, - Set oldLocationsToUpdate, Map> newAliases, - Map> oldAliases, Location outdatedPrefix, + protected @NonNull Set updateOutdatedLocations(Services services, + @NonNull Set oldLocationsToUpdate, + @NonNull Map> newAliases, + @NonNull Map> oldAliases, Location outdatedPrefix, ReferencePrefix thisReference) { // Ensure that at least one possibly outdated location is available. if (!oldLocationsToUpdate.isEmpty()) { diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/ThinBackwardSlicer.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/ThinBackwardSlicer.java index 064224c2228..444d9c8b65f 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/ThinBackwardSlicer.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/ThinBackwardSlicer.java @@ -23,6 +23,8 @@ import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableArray; +import org.jspecify.annotations.NonNull; + /** * Implementation of thin backward slicing. * @@ -33,8 +35,10 @@ public class ThinBackwardSlicer extends AbstractBackwardSlicer { * {@inheritDoc} */ @Override - protected boolean accept(Node node, Node previousChild, Services services, - Set relevantLocations, SequentInfo info, SourceElement activeStatement) + protected boolean accept(@NonNull Node node, @NonNull Node previousChild, + @NonNull Services services, + @NonNull Set relevantLocations, @NonNull SequentInfo info, + SourceElement activeStatement) throws ProofInputException { try { boolean accept = false; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/package-info.java new file mode 100644 index 00000000000..e08dc6f4a2e --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.slicing; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractHitCountBreakpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractHitCountBreakpoint.java index 15e6b7890cc..7fbc7705acb 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractHitCountBreakpoint.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractHitCountBreakpoint.java @@ -12,6 +12,8 @@ import org.key_project.prover.rules.RuleApp; +import org.jspecify.annotations.NonNull; + /** * Adds the hit count functionality to an {@link AbstractBreakpoint}. * @@ -52,7 +54,7 @@ protected AbstractHitCountBreakpoint(int hitCount, Proof proof, boolean enabled) * * @return true if the Hitcount is exceeded or the {@link LineBreakpoint} has no Hitcount. */ - protected boolean hitcountExceeded(Node node) { + protected boolean hitcountExceeded(@NonNull Node node) { if (!(hitCount == -1)) { if (!hittedNodes.containsKey(node.serialNr())) { if (hitCount == hitted + 1) { diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/ExceptionBreakpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/ExceptionBreakpoint.java index de27cb64c96..9068af18299 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/ExceptionBreakpoint.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/ExceptionBreakpoint.java @@ -18,6 +18,9 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * This{@link ExceptionBreakpoint} represents an exception breakpoint and is responsible to tell the * debugger to stop execution when the respective breakpoint is hit. @@ -33,7 +36,7 @@ public class ExceptionBreakpoint extends AbstractHitCountBreakpoint { /** * a list of nodes of the Symbolic Execution Tree whose children represent exceptions */ - private final Set exceptionParentNodes; + private final @NonNull Set exceptionParentNodes; /** * a flag whether to watch for an uncaught exception @@ -79,7 +82,7 @@ public ExceptionBreakpoint(Proof proof, String exceptionName, boolean caught, bo * @param parent The {@link Node} that is thought to be the parent. * @return true if the parent node is one of the nodes parents */ - public boolean isParentNode(Node node, Node parent) { + public boolean isParentNode(@Nullable Node node, Node parent) { if (node != null) { Node parentIter = node.parent(); boolean result = false; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/FieldWatchpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/FieldWatchpoint.java index 31bcda64eca..5c04aeb2c7d 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/FieldWatchpoint.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/FieldWatchpoint.java @@ -16,6 +16,8 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.PosInOccurrence; +import org.jspecify.annotations.NonNull; + /** * This{@link FieldWatchpoint} represents a Java watchpoint and is responsible to tell the debugger * to stop execution when the respective variable is accessed or modified. @@ -27,7 +29,7 @@ public class FieldWatchpoint extends AbstractHitCountBreakpoint { private boolean isModification; - private final String fullFieldName; + private final @NonNull String fullFieldName; /** * Creates a new {@link FieldWatchpoint}. @@ -41,7 +43,7 @@ public class FieldWatchpoint extends AbstractHitCountBreakpoint { * @param proof the {@link Proof} that will be executed and should stop */ public FieldWatchpoint(boolean enabled, int hitCount, String fieldName, boolean isAcces, - boolean isModification, KeYJavaType containerKJT, Proof proof) { + boolean isModification, @NonNull KeYJavaType containerKJT, Proof proof) { super(hitCount, proof, enabled); this.isAccess = isAcces; this.isModification = isModification; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/KeYWatchpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/KeYWatchpoint.java index 26ff26cc2c9..9dbaa2885ca 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/KeYWatchpoint.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/KeYWatchpoint.java @@ -28,6 +28,7 @@ import org.key_project.prover.sequent.Sequent; + /** * This{@link KeYWatchpoint} represents a KeY watchpoint and is responsible to tell the debugger to * stop execution when the respective watchpoint evaluates its condition to true. diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/LineBreakpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/LineBreakpoint.java index 80d8e74e65e..d115538eb9f 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/LineBreakpoint.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/LineBreakpoint.java @@ -20,6 +20,9 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.util.ExtList; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + public class LineBreakpoint extends AbstractConditionalBreakpoint { /** * The path of the class this {@link LineBreakpoint} is associated with. @@ -57,7 +60,8 @@ public class LineBreakpoint extends AbstractConditionalBreakpoint { * @param methodEnd the line the containing method of this breakpoint ends at * @throws SLTranslationException if the condition could not be parsed to a valid Term */ - public LineBreakpoint(String classPath, int lineNumber, int hitCount, IProgramMethod pm, + public LineBreakpoint(String classPath, int lineNumber, int hitCount, + @NonNull IProgramMethod pm, Proof proof, String condition, boolean enabled, boolean conditionEnabled, int methodStart, int methodEnd) throws SLTranslationException { super(hitCount, pm, proof, enabled, conditionEnabled, methodStart, methodEnd, @@ -80,7 +84,8 @@ public LineBreakpoint(String classPath, int lineNumber, int hitCount, IProgramMe * Breakpoint */ @Override - protected StatementBlock getStatementBlock(StatementContainer statementContainer) { + protected @NonNull StatementBlock getStatementBlock( + @NonNull StatementContainer statementContainer) { // list of all statements ExtList nextResult = new ExtList(); for (int i = 0; i < statementContainer.getStatementCount(); i++) { @@ -124,7 +129,7 @@ public boolean isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, N && super.isBreakpointHit(activeStatement, ruleApp, node); } - private boolean isInLine(SourceElement activeStatement) { + private boolean isInLine(@Nullable SourceElement activeStatement) { if (activeStatement != null && activeStatement.getStartPosition() != Position.UNDEFINED) { final String path = Paths.get(activeStatement.getPositionInfo().getParentClassURI()).toString(); diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/SymbolicExecutionExceptionBreakpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/SymbolicExecutionExceptionBreakpoint.java index a6bde67e0d5..3b72f6b5f9c 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/SymbolicExecutionExceptionBreakpoint.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/SymbolicExecutionExceptionBreakpoint.java @@ -20,6 +20,9 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * This{@link SymbolicExecutionExceptionBreakpoint} represents an exception breakpoint and is * responsible to tell the debugger to stop execution when the respective breakpoint is hit. @@ -35,12 +38,12 @@ public class SymbolicExecutionExceptionBreakpoint extends AbstractHitCountBreakp /** * a Set of Nodes that represent exceptions */ - private final Set exceptionNodes; + private final @NonNull Set exceptionNodes; /** * a list of nodes of the Symbolic Execution Tree whose children represent exceptions */ - private final Set exceptionParentNodes; + private final @NonNull Set exceptionParentNodes; /** * a flag whether to watch for an uncaught exception @@ -125,7 +128,7 @@ public void updateState(Goal goal, int maxApplications, long timeout, long start * @param parent The {@link Node} that is thought to be the parent. * @return true if the parent node is one of the nodes parents */ - public boolean isParentNode(Node node, Node parent) { + public boolean isParentNode(@Nullable Node node, Node parent) { if (node != null) { Node parentIter = node.parent(); boolean result = false; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/package-info.java new file mode 100644 index 00000000000..32236c3757e --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.strategy.breakpoint; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/package-info.java new file mode 100644 index 00000000000..a0126ddce2d --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.strategy; 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 2cf2b632cd3..027291d1bb2 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 @@ -42,7 +42,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/main/java/de/uka/ilkd/key/symbolic_execution/util/SideProofStore.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SideProofStore.java index 5e068334a5c..849c6b950e1 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SideProofStore.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SideProofStore.java @@ -18,6 +18,9 @@ import org.key_project.util.java.CollectionUtil; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** *

* The only instance of this class {@link #DEFAULT_INSTANCE} is used to manage performed side @@ -96,7 +99,7 @@ public void setEnabled(boolean enabled) { * @param description The description. * @param proof The {@link Proof} to add. */ - public void addProof(String description, Proof proof) { + public void addProof(String description, @NonNull Proof proof) { synchronized (entries) { if (!containsEntry(proof)) { Entry entry = new Entry(description, proof); @@ -113,7 +116,7 @@ public void addProof(String description, Proof proof) { * * @param entries The {@link Entry}s to remove. */ - public void removeEntries(Collection entries) { + public void removeEntries(@NonNull Collection entries) { synchronized (entries) { if (this.entries.removeAll(entries)) { for (Entry entry : entries) { @@ -148,7 +151,7 @@ public boolean containsEntry(Proof proof) { * @param proof The {@link Proof} for which the {@link Entry} is requested. * @return The {@link Entry} with the given {@link Proof} or {@code null} if not available. */ - public Entry getEntry(final Proof proof) { + public @Nullable Entry getEntry(final Proof proof) { return CollectionUtil.search(entries, element -> element != null && element.getProof() == proof); } @@ -179,7 +182,7 @@ public int countEntries() { * @param index The index. * @return The {@link Entry} at the given index. */ - public Entry getEntryAt(int index) { + public @Nullable Entry getEntryAt(int index) { return index >= 0 && index < entries.size() ? entries.get(index) : null; } @@ -188,7 +191,7 @@ public Entry getEntryAt(int index) { * * @return All available {@link Entry}s. */ - public Entry[] getEntries() { + public Entry @NonNull [] getEntries() { return entries.toArray(new Entry[0]); } @@ -197,7 +200,7 @@ public Entry[] getEntries() { * * @param l The {@link ISideProofStoreListener} to register. */ - public void addProofStoreListener(ISideProofStoreListener l) { + public void addProofStoreListener(@Nullable ISideProofStoreListener l) { if (l != null) { listener.add(l); } @@ -208,7 +211,7 @@ public void addProofStoreListener(ISideProofStoreListener l) { * * @param l The {@link ISideProofStoreListener} to unregister. */ - public void removeProofStoreListener(ISideProofStoreListener l) { + public void removeProofStoreListener(@Nullable ISideProofStoreListener l) { if (l != null) { listener.remove(l); } @@ -219,7 +222,7 @@ public void removeProofStoreListener(ISideProofStoreListener l) { * * @return All registered {@link ISideProofStoreListener}. */ - public ISideProofStoreListener[] getProofStoreListener() { + public ISideProofStoreListener @NonNull [] getProofStoreListener() { return listener.toArray(new ISideProofStoreListener[0]); } @@ -304,7 +307,7 @@ public static class Entry { /** * The {@link KeYEnvironment}. */ - private final KeYEnvironment environment; + private final @NonNull KeYEnvironment environment; /** * Constructor. @@ -312,7 +315,7 @@ public static class Entry { * @param description The description. * @param proof The {@link Proof}. */ - public Entry(String description, Proof proof) { + public Entry(String description, @NonNull Proof proof) { this.description = description; this.proof = proof; DefaultUserInterfaceControl ui = new DefaultUserInterfaceControl(); diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionEnvironment.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionEnvironment.java index 3111f1628df..3bc264adc4b 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionEnvironment.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionEnvironment.java @@ -14,6 +14,9 @@ import de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionGoalChooser; import de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionStrategy; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * Instances of this class are used to collect and access all relevant information for symbolic * execution tree extraction of {@link Proof}s via an {@link SymbolicExecutionTreeBuilder}. @@ -33,7 +36,7 @@ public class SymbolicExecutionEnvironment * @param environment The parent {@link KeYEnvironment}. * @param builder The {@link SymbolicExecutionTreeBuilder} for execution tree extraction. */ - public SymbolicExecutionEnvironment(KeYEnvironment environment, + public SymbolicExecutionEnvironment(@NonNull KeYEnvironment environment, SymbolicExecutionTreeBuilder builder) { this(environment.getUi(), environment.getInitConfig(), builder); } @@ -45,7 +48,7 @@ public SymbolicExecutionEnvironment(KeYEnvironment environment, * @param initConfig The loaded project. * @param builder The {@link SymbolicExecutionTreeBuilder} for execution tree extraction. */ - public SymbolicExecutionEnvironment(U ui, InitConfig initConfig, + public SymbolicExecutionEnvironment(@NonNull U ui, @NonNull InitConfig initConfig, SymbolicExecutionTreeBuilder builder) { super(ui, initConfig); this.builder = builder; @@ -110,7 +113,7 @@ public static void configureProofForSymbolicExecution(Proof proof, * side proofs, {@code false} do not hide execution branch labels. * @param aliasChecks Do alias checks? */ - public static void configureProofForSymbolicExecution(Proof proof, + public static void configureProofForSymbolicExecution(@Nullable Proof proof, int maximalNumberOfNodesPerBranch, boolean methodTreatmentContract, boolean loopTreatmentInvariant, boolean blockTreatmentContract, boolean nonExecutionBranchHidingSideProofs, boolean aliasChecks) { diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/event/SideProofStoreEvent.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/event/SideProofStoreEvent.java index d235c5f6fa7..d13e648dd84 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/event/SideProofStoreEvent.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/event/SideProofStoreEvent.java @@ -8,6 +8,8 @@ import de.uka.ilkd.key.symbolic_execution.util.SideProofStore; import de.uka.ilkd.key.symbolic_execution.util.SideProofStore.Entry; +import org.jspecify.annotations.NonNull; + /** * An event thrown by a {@link SideProofStore} and observed via an {@link ISideProofStoreListener}. * @@ -30,7 +32,7 @@ public class SideProofStoreEvent extends EventObject { * @param source The source. * @param entries The added or removed {@link Entry}s. */ - public SideProofStoreEvent(SideProofStore source, Entry[] entries) { + public SideProofStoreEvent(@NonNull SideProofStore source, Entry[] entries) { super(source); this.entries = entries; } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/event/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/event/package-info.java new file mode 100644 index 00000000000..f85353a243f --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/event/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.util.event; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/package-info.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/package-info.java new file mode 100644 index 00000000000..599248a77de --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/package-info.java @@ -0,0 +1,2 @@ +@org.jspecify.annotations.NullMarked +package de.uka.ilkd.key.symbolic_execution.util; 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 4631b89e3ac..3e7a8f3ec6d 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 @@ -10,6 +10,7 @@ import de.uka.ilkd.key.symbolic_execution.util.EqualsHashCodeResetter; +import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.Test; import static org.junit.jupiter.api.Assertions.*; @@ -251,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) { + public boolean equals(@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 5110ebe93a4..02345fe61d1 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 61363156d72..3561ebc6d8e 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 8bbb3a753d2..494d03ffba6 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.proof.Goal; @@ -22,11 +23,12 @@ import org.key_project.prover.strategy.costbased.RuleAppCost; import org.jspecify.annotations.NonNull; +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 @@ -41,7 +43,7 @@ public String getName() { @Override public String getCategory() { - return null; + return ""; } @@ -57,8 +59,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<>(); unwindRules.add("loopUnwind"); @@ -69,7 +74,7 @@ class TestGenStrategy extends FilterStrategy { 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 a42295d232f..43b6a68ad8c 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 @@ -44,6 +44,7 @@ import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -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/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java index 39b5d178428..dabcd914429 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 @@ -208,7 +208,7 @@ public String getMUTCall() { params.append(",").append(var.name()); } } - if (params.length() > 0) { + if (!params.isEmpty()) { params = new StringBuilder(params.substring(1)); } @@ -323,8 +323,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 315a096190d..1764ac2835e 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 9df726acd4a..d57b622d1da 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -267,3 +267,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/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 15e9da63b38..a0fe58fed1c 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. */ protected 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 JTerm getDefiningAxiom(JTerm varOrConst, Services services) { return tb.tt(); } - if (predicates.size() == 0) { + if (predicates.isEmpty()) { return tb.ff(); } @@ -125,7 +128,7 @@ public JTerm getDefiningAxiom(JTerm 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/ConjunctivePredicateAbstractionDomainElement.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionDomainElement.java index ca226a49d12..51696edf298 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 e57ebc5de1b..3d0f0c9c421 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 842306e21b4..feb1b125579 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 6eedd343e94..68f89f4d7cd 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 @@ -31,6 +31,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; @@ -45,7 +46,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 @@ -83,7 +84,7 @@ protected AbstractProofControl(ProverTaskListener defaultProverTaskListener) { * @param ruleCompletionHandler An optional {@link RuleCompletionHandler}. */ protected AbstractProofControl(ProverTaskListener defaultProverTaskListener, - RuleCompletionHandler ruleCompletionHandler) { + @Nullable RuleCompletionHandler ruleCompletionHandler) { this.ruleCompletionHandler = ruleCompletionHandler; this.defaultProverTaskListener = defaultProverTaskListener; } @@ -157,8 +158,7 @@ public ImmutableList getRewriteTaclet(Goal focusedGoal, * TacletApps */ private ImmutableList filterTaclet(Goal focusedGoal, - ImmutableList tacletInstances, - PosInOccurrence pos) { + ImmutableList tacletInstances, @Nullable PosInOccurrence pos) { HashSet applicableRules = new 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 c8a26ca1100..7f689ab96a5 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 @@ -28,6 +28,7 @@ import org.key_project.prover.engine.TaskFinishedInfo; import org.key_project.prover.engine.TaskStartedInfo; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -207,10 +208,14 @@ public void taskFinished(TaskFinishedInfo info) { * {@inheritDoc} */ @Override - public AbstractProblemLoader load(Profile profile, Path file, List classPath, - Path bootClassPath, List includes, Properties poPropertiesToForce, + public AbstractProblemLoader load(@Nullable Profile profile, + @Nullable Path file, + @Nullable List classPath, + @Nullable Path 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, @@ -257,7 +262,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 cb3cbd0ffe4..bb13cecc1a9 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.prover.sequent.PosInOccurrence; 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,11 +113,9 @@ 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); - starter.init(proof); + ProofStarter starter = new ProofStarter.Builder( + new CompositePTListener(getDefaultProverTaskListener(), ptl), false) + .build(proof); if (goals != null) { starter.start(goals); } else { 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 79cf93a6af6..baae1d811e7 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 @@ -29,6 +29,7 @@ import org.key_project.util.collection.ImmutableSet; +import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; /** @@ -41,7 +42,7 @@ public class KeYEnvironment { /** * The {@link UserInterfaceControl} in which the {@link Proof} is loaded. */ - private final U ui; + private final @NonNull U ui; /** * The loaded project. @@ -51,7 +52,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. @@ -66,7 +67,7 @@ public class KeYEnvironment { /** * The {@link ReplayResult} if available. */ - private final ReplayResult replayResult; + private final @Nullable ReplayResult replayResult; /** * Constructor @@ -74,7 +75,7 @@ public class KeYEnvironment { * @param ui The {@link UserInterfaceControl} in which the {@link Proof} is loaded. * @param initConfig The loaded project. */ - public KeYEnvironment(U ui, InitConfig initConfig) { + public KeYEnvironment(@NonNull U ui, InitConfig initConfig) { this(ui, initConfig, null, null, null); } @@ -85,8 +86,8 @@ public KeYEnvironment(U ui, InitConfig initConfig) { * @param initConfig The loaded project. * @param proofScript add an optional proof script */ - public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof, - @Nullable ProofScript proofScript, ReplayResult replayResult) { + public KeYEnvironment(@NonNull U ui, InitConfig initConfig, @Nullable Proof loadedProof, + @Nullable ProofScript proofScript, @Nullable ReplayResult replayResult) { this.ui = ui; this.initConfig = initConfig; this.loadedProof = loadedProof; @@ -99,7 +100,7 @@ public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof, * * @return The {@link UserInterfaceControl} in which the {@link Proof} is loaded. */ - public U getUi() { + public @NonNull U getUi() { return ui; } @@ -157,7 +158,7 @@ public Profile getProfile() { * * @return The loaded {@link Proof} if available and {@code null} otherwise. */ - public Proof getLoadedProof() { + public @Nullable Proof getLoadedProof() { return loadedProof; } @@ -166,7 +167,7 @@ public Proof getLoadedProof() { * * @return The {@link ReplayResult} or {@code null} if not available. */ - public ReplayResult getReplayResult() { + public @Nullable ReplayResult getReplayResult() { return replayResult; } @@ -193,7 +194,8 @@ public Proof createProof(ProofOblInput input) throws ProofInputException { * @throws ProblemLoaderException Occurred Exception */ public static KeYEnvironment load(Path location, - List classPaths, Path bootClassPath, List includes) + @Nullable List classPaths, @Nullable Path bootClassPath, + @Nullable List includes) throws ProblemLoaderException { return load(null, location, classPaths, bootClassPath, includes, false); } @@ -234,7 +236,8 @@ public static KeYEnvironment load(Path location, * @throws ProblemLoaderException Occurred Exception */ public static KeYEnvironment load(Profile profile, Path location, - List classPaths, Path bootClassPath, List includes, + @Nullable List classPaths, @Nullable Path bootClassPath, + @Nullable List includes, boolean forceNewProfileOfNewProofs) throws ProblemLoaderException { return load(profile, location, classPaths, bootClassPath, includes, null, null, forceNewProfileOfNewProofs); @@ -260,9 +263,11 @@ 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, Path location, - List classPaths, Path bootClassPath, List includes, - Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler, + public static KeYEnvironment load(Profile profile, + @Nullable Path location, + @Nullable List classPaths, @Nullable Path bootClassPath, + @Nullable List includes, + @Nullable Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler, boolean forceNewProfileOfNewProofs) throws ProblemLoaderException { return load(profile, location, classPaths, bootClassPath, includes, poPropertiesToForce, ruleCompletionHandler, @@ -290,9 +295,11 @@ public static KeYEnvironment load(Profile profile, * @throws ProblemLoaderException Occurred Exception */ public static KeYEnvironment load(Profile profile, Path location, - List classPaths, Path bootClassPath, List includes, - Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler, - Consumer callbackProofLoaded, + @Nullable List classPaths, @Nullable Path bootClassPath, + @Nullable List includes, + @Nullable Properties poPropertiesToForce, + @Nullable RuleCompletionHandler ruleCompletionHandler, + @Nullable Consumer callbackProofLoaded, boolean forceNewProfileOfNewProofs) throws ProblemLoaderException { DefaultUserInterfaceControl ui = new DefaultUserInterfaceControl(ruleCompletionHandler); 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 070c9e6cb51..2bd7d8b7db7 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 @@ -20,6 +20,8 @@ import org.key_project.prover.engine.ProverTaskListener; +import org.jspecify.annotations.Nullable; + /** * Provides the user interface independent logic to manage multiple proofs. This includes: *