Merge remote-tracking branch 'upstream/eisop/keycore2' into eisop/key…

…core2

key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java

@@ -81,7 +81,7 @@ public class InitConfig {
 
     private String originalKeYFileName;
 
-    private ProofSettings settings;
+    private @Nullable ProofSettings settings;
 
 
 
@@ -118,6 +118,7 @@ public final Services getServices() {
     }
 
 
+    @Pure
     public Profile getProfile() {
         return services.getProfile();
     }
@@ -394,7 +395,7 @@ public Namespace<Choice> choiceNS() {
     }
 
 
-    public void setSettings(ProofSettings newSettings) {
+    public void setSettings(@Nullable ProofSettings newSettings) {
         this.settings = newSettings;
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofOblInput.java

@@ -5,6 +5,7 @@
 
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.proof.ProofAggregate;
+import org.jspecify.annotations.Nullable;
 
 
 /**
@@ -37,5 +38,5 @@ public interface ProofOblInput {
      * @return The {@link KeYJavaType} in which the proven element is contained in or {@code null}
      *         if not available.
      */
-    KeYJavaType getContainerType();
+    @Nullable KeYJavaType getContainerType();
 }

key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java

@@ -71,7 +71,7 @@ public static void setDefaultValues(int saveInterval, boolean saveClosedProof) {
      * Create a new instance using default values, or null if auto save is disabled by default. The
      * default values can be set through <code>AutoSaver.setDefaultValues()</code>
      */
-    public static AutoSaver getDefaultInstance() {
+    public static @Nullable AutoSaver getDefaultInstance() {
         return DEFAULT_INSTANCE;
     }
 
@@ -99,7 +99,7 @@ public AutoSaver(int saveInterval, boolean saveClosedProof) {
      *
      * @param p proof to save, must not be null
      */
-    public void setProof(Proof p) {
+    public void setProof(@Nullable Proof p) {
         proof = p;
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java

@@ -825,11 +825,11 @@ public static String printTerm(Term t, @Nullable Services serv, boolean shortAtt
         return logicPrinter.result();
     }
 
-    public static String printAnything(Object val, Services services) {
+    public static @Nullable String printAnything(Object val, @Nullable Services services) {
         return printAnything(val, services, true);
     }
 
-    public static String printAnything(Object val, Services services,
+    public static @Nullable String printAnything(@Nullable Object val, @Nullable Services services,
             boolean shortAttrNotation) {
         if (val instanceof ProgramElement) {
             return printProgramElement((ProgramElement) val);
@@ -850,7 +850,7 @@ public static String printAnything(Object val, Services services,
         }
     }
 
-    private static String printSequent(Sequent val, Services services) {
+    private static String printSequent(Sequent val, @Nullable Services services) {
         final LogicPrinter printer = createLogicPrinter(services, services == null);
         printer.printSequent(val);
         return printer.result();

key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java

@@ -17,9 +17,9 @@
 
 public class RuleJustificationInfo {
 
-    private final Map<RuleKey, RuleJustification> rule2Justification = new LinkedHashMap<>();
+    private final Map<RuleKey, @Nullable RuleJustification> rule2Justification = new LinkedHashMap<>();
 
-    public void addJustification(Rule r, RuleJustification j) {
+    public void addJustification(Rule r, @Nullable RuleJustification j) {
         final RuleKey ruleKey = new RuleKey(r);
         if (rule2Justification.containsKey(ruleKey)) {
             // TODO: avoid double registration of certain class axioms and remove then the below

key.core/src/main/java/de/uka/ilkd/key/util/DirectoryFileCollection.java

@@ -14,6 +14,7 @@
 
 import de.uka.ilkd.key.proof.io.consistency.FileRepo;
 
+import org.jspecify.annotations.Nullable;
 import recoder.io.DataFileLocation;
 import recoder.io.DataLocation;
 
@@ -46,7 +47,7 @@ public DirectoryFileCollection(File directory) {
     /*
      * add all files in or under dir to a file list. Extension is tested
      */
-    private static void addAllFiles(File dir, String extension, List<File> files) {
+    private static void addAllFiles(File dir, @Nullable String extension, List<File> files) {
         File[] listFiles = dir.listFiles();
 
         if (listFiles == null) {
@@ -132,7 +133,7 @@ public Walker createWalker(String[] extensions) {
     private static class Walker implements FileCollection.Walker {
 
         private final Iterator<File> iterator;
-        private File currentFile;
+        private @Nullable File currentFile;
 
         public Walker(Iterator<File> iterator) {
             this.iterator = iterator;
@@ -157,10 +158,10 @@ public InputStream openCurrent() throws IOException {
 
         @Override
         public InputStream openCurrent(FileRepo fileRepo) throws IOException {
-            if (fileRepo != null) {
-                return fileRepo.getInputStream(currentFile.toPath());
+            if (currentFile == null) {
+                throw new NoSuchElementException();
             } else {
-                return openCurrent(); // fallback without FileRepo
+                return fileRepo.getInputStream(currentFile.toPath());
             }
         }
 

key.core/src/main/java/de/uka/ilkd/key/util/HelperClassForTests.java

@@ -302,7 +302,9 @@ public static IProgramMethod searchProgramMethod(Services services, String conta
     }
 
     public static Services createServices(File keyFile) {
-        JavaInfo javaInfo = new HelperClassForTests().parse(keyFile).getFirstProof().getJavaInfo();
+        Proof proof = new HelperClassForTests().parse(keyFile).getFirstProof();
+        assert proof != null;
+        JavaInfo javaInfo = proof.getJavaInfo();
         return javaInfo.getServices();
     }
 

key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java

@@ -5,6 +5,7 @@
 
 import java.util.HashMap;
 import java.util.Map;
+import java.util.Objects;
 
 import de.uka.ilkd.key.java.JavaProgramElement;
 import de.uka.ilkd.key.java.Services;
@@ -18,6 +19,7 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.VariableNameProposer;
 
+import org.jspecify.annotations.Nullable;
 import org.key_project.logic.Name;
 import org.key_project.logic.op.Function;
 
@@ -46,7 +48,7 @@ public class InfFlowProgVarRenamer extends TermBuilder {
     private final Goal goalForVariableRegistration;
 
 
-    public InfFlowProgVarRenamer(Term[] terms, Map<Term, Term> preInitialisedReplaceMap,
+    public InfFlowProgVarRenamer(Term[] terms, @Nullable Map<Term, Term> preInitialisedReplaceMap,
             String postfix, Goal goalForVariableRegistration, Services services) {
         super(services.getTermFactory(), services);
         this.terms = terms;
@@ -88,14 +90,10 @@ private Term renameVariablesAndSkolemConstants(Term term) {
 
 
     private Term renameFormulasWithoutPrograms(Term term) {
-        if (term == null) {
-            return null;
-        }
-
         if (!replaceMap.containsKey(term)) {
             renameAndAddToReplaceMap(term);
         }
-        return replaceMap.get(term);
+        return Objects.requireNonNull(replaceMap.get(term));
     }
 
 

key.core/src/main/java/de/uka/ilkd/key/util/KeYResourceManager.java

@@ -30,9 +30,9 @@ public class KeYResourceManager {
     private static final KeYResourceManager instance = new KeYResourceManager();
 
 
-    private String version = null;
-    private String sha1 = null;
-    private String branch = null;
+    private @Nullable String version;
+    private @Nullable String sha1;
+    private @Nullable String branch;
 
     private KeYResourceManager() {
     }
@@ -48,7 +48,7 @@ public static KeYResourceManager getManager() {
     /**
      * reads a version string or returns "x.z.y" in case of failures
      */
-    private String readVersionString(URL url) {
+    private String readVersionString(@Nullable URL url) {
         StringBuilder result = new StringBuilder();
         if (url != null) {
             try (InputStream io = new BufferedInputStream(url.openStream())) {
@@ -209,7 +209,7 @@ public boolean copy(Class<?> cl, String resourcename, String targetLocation,
      * @param resourcename the String that contains the name of the resource
      * @return the URL of the resource
      */
-    public URL getResourceFile(Object o, String resourcename) {
+    public @Nullable URL getResourceFile(Object o, String resourcename) {
         return getResourceFile(o.getClass(), resourcename);
     }
 

key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java

@@ -274,7 +274,7 @@ public ElementWrapper(K key, Property<K> property) {
         }
 
         @Override
-        public boolean equals(@org.jspecify.annotations.Nullable Object obj) {
+        public boolean equals(@Nullable Object obj) {
             if (obj instanceof ElementWrapper<?> other) {
                 return key.equalsModProperty(other.key, property);
             }

key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java

@@ -89,7 +89,7 @@ private MiscTools() {
      * @return The {@link LoopSpecification} for the loop statement in the given term or an empty
      *         optional if there is no specified invariant for the loop.
      */
-    public static LoopSpecification getSpecForTermWithLoopStmt(final Term loopTerm,
+    public static @Nullable LoopSpecification getSpecForTermWithLoopStmt(final Term loopTerm,
             final Services services) {
         assert loopTerm.op() instanceof Modality;
         assert loopTerm.javaBlock() != JavaBlock.EMPTY_JAVABLOCK;
@@ -870,6 +870,7 @@ public static URI parseURL(@Nullable String input) throws URISyntaxException {
         if (m.matches() && m.groupCount() == 2) {
             scheme = Objects.requireNonNull(m.group(1));
             schemeSpecPart = m.group(2);
+            assert schemeSpecPart != null;
         }
         switch (scheme) {
         case "URL" -> {

key.core/src/main/java/de/uka/ilkd/key/util/ProofStarter.java

@@ -28,6 +28,7 @@
 import de.uka.ilkd.key.strategy.StrategyFactory;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 
+import org.jspecify.annotations.Nullable;
 import org.key_project.util.collection.ImmutableList;
 
 /**
@@ -49,13 +50,13 @@ public static class UserProvidedInput implements ProofOblInput {
         private static final String EMPTY_PROOF_HEADER = "";
         private final ProofEnvironment env;
         private final Sequent seq;
-        private final String proofName;
+        private final @Nullable String proofName;
 
         public UserProvidedInput(Sequent seq, ProofEnvironment env) {
             this(seq, env, null);
         }
 
-        public UserProvidedInput(Sequent seq, ProofEnvironment env, String proofName) {
+        public UserProvidedInput(Sequent seq, ProofEnvironment env, @Nullable String proofName) {
             this.seq = seq;
             this.env = env;
             this.proofName = proofName;
@@ -105,22 +106,22 @@ public boolean implies(ProofOblInput po) {
          * {@inheritDoc}
          */
         @Override
-        public KeYJavaType getContainerType() {
+        public @Nullable KeYJavaType getContainerType() {
             return null;
         }
     }
 
-    private Proof proof;
+    private @Nullable Proof proof;
 
     private int maxSteps = 2000;
 
     private long timeout = -1L;
 
-    private final ProverTaskListener ptl;
+    private final @Nullable ProverTaskListener ptl;
 
-    private AutoSaver autoSaver;
+    private @Nullable AutoSaver autoSaver;
 
-    private Strategy strategy;
+    private @Nullable Strategy strategy;
 
     /**
      * creates an instance of the ProofStarter
@@ -137,7 +138,7 @@ public ProofStarter(boolean useAutoSaver) {
      * @param ptl the ProverTaskListener to be informed about certain events
      * @param useAutoSaver boolean indicating whether the proof shall be auto saved
      */
-    public ProofStarter(ProverTaskListener ptl, boolean useAutoSaver) {
+    public ProofStarter(@Nullable ProverTaskListener ptl, boolean useAutoSaver) {
         this.ptl = ptl;
         if (useAutoSaver) {
             autoSaver = AutoSaver.getDefaultInstance();
@@ -152,6 +153,7 @@ public ProofStarter(ProverTaskListener ptl, boolean useAutoSaver) {
     public void init(Term formulaToProve, ProofEnvironment env) throws ProofInputException {
         final ProofOblInput input = new UserProvidedInput(formulaToProve, env);
         proof = input.getPO().getFirstProof();
+        assert proof != null;
         proof.setEnv(env);
     }
 
@@ -164,6 +166,7 @@ public void init(Sequent sequentToProve, ProofEnvironment env, String proofName)
             throws ProofInputException {
         final ProofOblInput input = new UserProvidedInput(sequentToProve, env, proofName);
         proof = input.getPO().getFirstProof();
+        assert proof != null;
         proof.setEnv(env);
     }
 
@@ -199,6 +202,7 @@ public void setStrategy(Strategy strategy) {
     }
 
     public void setStrategyProperties(StrategyProperties sp) {
+        assert proof != null;
         final Profile profile = proof.getInitConfig().getProfile();
         StrategyFactory factory = strategy != null ? profile.getStrategyFactory(strategy.name())
                 : profile.getDefaultStrategyFactory();
@@ -211,6 +215,7 @@ public void setStrategyProperties(StrategyProperties sp) {
      * @return the proof after the attempt terminated
      */
     public ApplyStrategyInfo start() {
+        assert proof != null;
         return start(proof.openGoals());
     }
 
@@ -220,6 +225,7 @@ public ApplyStrategyInfo start() {
      * @return the proof after the attempt terminated
      */
     public ApplyStrategyInfo start(ImmutableList<Goal> goals) {
+        assert proof != null;
         try {
             final Profile profile = proof.getInitConfig().getProfile();
 
@@ -284,7 +290,7 @@ public void init(Proof proof) {
      *
      * @return The managed side {@link Proof}.
      */
-    public Proof getProof() {
+    public @Nullable Proof getProof() {
         return proof;
     }
 }