module-info.java, 2nd attempt

build.gradle

@@ -74,6 +74,9 @@ subprojects {
         maven {
             url = 'https://git.key-project.org/api/v4/projects/35/packages/maven'
         }
+        maven { // remove if docking frames 1.1.3p5 on Maven Central
+            url "https://central.sonatype.com/repository/maven-snapshots"
+        }
     }
 
     dependencies {
@@ -513,8 +516,6 @@ tasks.register('alldoc', Javadoc){
         bottom = "Copyright &copy; 2003-2023 <a href=\"http://key-project.org\">The KeY-Project</a>."
         use = true
         links += "https://docs.oracle.com/en/java/javase/17/docs/api/"
-        links += "http://www.antlr2.org/javadoc/"
-        links += "http://www.antlr3.org/api/Java/"
         links += "https://www.antlr.org/api/Java/"
     }
 }

key.core.example/src/main/java/module-info.java

@@ -0,0 +1,13 @@
+import org.jspecify.annotations.NullMarked;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (31.03.24)
+ */
+@NullMarked module key.core.example {
+    requires org.jspecify;
+    requires org.slf4j;
+    requires key.core;
+    requires org.key_project.util;
+}

key.core.example/src/main/java/org/key_project/Main.java

@@ -57,7 +57,8 @@ public static void main(String[] args) {
      *
      * @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
+     * @return the {@link KeYEnvironment} that provides the context for all following verification
+     *         tasks
      * @throws ProblemLoaderException if the setup fails
      */
     private static KeYEnvironment<?> setupEnvironment(Path location) throws ProblemLoaderException {

key.core.proof_references/src/main/java/module-info.java

@@ -0,0 +1,14 @@
+import org.jspecify.annotations.NullMarked;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (31.03.24)
+ */
+@NullMarked module key.core.proof_references {
+    requires key.core;
+    requires key.ncore;
+    requires org.key_project.util;
+    requires key.prover;
+    requires org.jspecify;
+}

key.core.rifl/src/main/java/module-info.java

@@ -0,0 +1,17 @@
+import org.jspecify.annotations.NullMarked;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (31.03.24)
+ */
+@NullMarked module key.core.rifl {
+    exports de.uka.ilkd.key.util.rifl;
+
+    requires key.core;
+    requires key.recoder;
+    requires java.xml;
+    requires org.slf4j;
+    requires org.key_project.util;
+    requires org.jspecify;
+}

key.core.symbolic_execution.example/src/main/java/module-info.java

@@ -0,0 +1,15 @@
+import org.jspecify.annotations.NullMarked;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (31.03.24)
+ */
+@NullMarked module key.core.symbolic_execution.example {
+    requires transitive key.core.symbolic_execution;
+    requires key.core;
+    requires org.key_project.util;
+    requires org.slf4j;
+    requires org.jspecify;
+    requires key.prover;
+}

key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java

@@ -113,7 +113,8 @@ public static void main(String[] args) {
                 // Optionally, add a more advanced stop conditions like breakpoints
                 CompoundStopCondition stopCondition = new CompoundStopCondition();
                 // Stop after 100 nodes have been explored on each branch.
-                stopCondition.addChildren(new ExecutedSymbolicExecutionTreeNodesStopCondition(100));
+                stopCondition.addChildren(
+                    new ExecutedSymbolicExecutionTreeNodesStopCondition(100));
                 // stopCondition.addChildren(new StepOverSymbolicExecutionTreeNodesStopCondition());
                 // // Perform only a step over
                 // stopCondition.addChildren(new

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/BlockContractValidityTermLabelUpdate.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.rule.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Set;
 
@@ -12,6 +12,7 @@
 import de.uka.ilkd.key.logic.label.TermLabelState;
 import de.uka.ilkd.key.rule.BlockContractInternalRule;
 import de.uka.ilkd.key.rule.LoopContractInternalRule;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
 import org.key_project.logic.Name;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelMerger.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.rule.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.ArrayList;
 import java.util.Arrays;
@@ -10,6 +10,7 @@
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.label.FormulaTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;
+import de.uka.ilkd.key.rule.label.TermLabelMerger;
 
 import org.key_project.prover.sequent.SequentFormula;
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelRefactoring.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.rule.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.*;
 
@@ -14,6 +14,8 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
+import de.uka.ilkd.key.rule.label.StayOnOperatorTermLabelPolicy;
+import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
 import de.uka.ilkd.key.rule.merge.CloseAfterMerge;
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelUpdate.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.rule.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Collections;
 import java.util.LinkedHashMap;
@@ -18,6 +18,7 @@
 import de.uka.ilkd.key.rule.Taclet.TacletLabelHint;
 import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation;
 import de.uka.ilkd.key.rule.TacletApp;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
 
 import org.key_project.logic.Name;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopBodyTermLabelUpdate.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/LoopBodyTermLabelUpdate.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.rule.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Set;
 
@@ -10,6 +10,7 @@
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelState;
 import de.uka.ilkd.key.rule.WhileInvariantRule;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
 import org.key_project.logic.Name;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopInvariantNormalBehaviorTermLabelUpdate.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/LoopInvariantNormalBehaviorTermLabelUpdate.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.rule.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Set;
 
@@ -10,6 +10,7 @@
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelState;
 import de.uka.ilkd.key.rule.WhileInvariantRule;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
 import org.key_project.logic.Name;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/RemoveInCheckBranchesTermLabelRefactoring.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/RemoveInCheckBranchesTermLabelRefactoring.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.rule.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.JTerm;
@@ -16,6 +16,7 @@
 import de.uka.ilkd.key.rule.LoopContractInternalRule;
 import de.uka.ilkd.key.rule.UseOperationContractRule;
 import de.uka.ilkd.key.rule.WhileInvariantRule;
+import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
 
 import org.key_project.logic.Name;
 import org.key_project.prover.rules.Rule;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/StayOnFormulaTermLabelPolicy.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.rule.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Deque;
 import java.util.LinkedHashSet;
@@ -16,6 +16,7 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.rule.Taclet.TacletLabelHint;
 import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation;
+import de.uka.ilkd.key.rule.label.TermLabelPolicy;
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
 
 import org.key_project.prover.rules.Rule;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/SymbolicExecutionTermLabelUpdate.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/SymbolicExecutionTermLabelUpdate.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.rule.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Set;
 
@@ -11,6 +11,7 @@
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelState;
 import de.uka.ilkd.key.rule.*;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 
 import org.key_project.logic.Name;
 import org.key_project.prover.rules.Rule;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java

@@ -18,20 +18,12 @@
 import de.uka.ilkd.key.proof.init.JavaProfile;
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.rule.BuiltInRule;
-import de.uka.ilkd.key.rule.label.BlockContractValidityTermLabelUpdate;
-import de.uka.ilkd.key.rule.label.FormulaTermLabelMerger;
-import de.uka.ilkd.key.rule.label.FormulaTermLabelRefactoring;
-import de.uka.ilkd.key.rule.label.FormulaTermLabelUpdate;
-import de.uka.ilkd.key.rule.label.LoopBodyTermLabelUpdate;
-import de.uka.ilkd.key.rule.label.LoopInvariantNormalBehaviorTermLabelUpdate;
-import de.uka.ilkd.key.rule.label.RemoveInCheckBranchesTermLabelRefactoring;
-import de.uka.ilkd.key.rule.label.StayOnFormulaTermLabelPolicy;
 import de.uka.ilkd.key.rule.label.StayOnOperatorTermLabelPolicy;
-import de.uka.ilkd.key.rule.label.SymbolicExecutionTermLabelUpdate;
 import de.uka.ilkd.key.rule.label.TermLabelPolicy;
 import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
 import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.strategy.StrategyFactory;
+import de.uka.ilkd.key.symbolic_execution.label.*;
 import de.uka.ilkd.key.symbolic_execution.rule.ModalitySideProofRule;
 import de.uka.ilkd.key.symbolic_execution.rule.QuerySideProofRule;
 import de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionGoalChooserFactory;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java

@@ -1,11 +1,12 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.proof;
+package de.uka.ilkd.key.symbolic_execution.proof;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.op.LocationVariable;
-import de.uka.ilkd.key.strategy.IBreakpointStopCondition;
+import de.uka.ilkd.key.proof.TermProgramVariableCollector;
+import de.uka.ilkd.key.symbolic_execution.strategy.*;
 import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractConditionalBreakpoint;
 import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint;
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/BreakpointStopCondition.java

@@ -12,7 +12,6 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.NodeInfo;
-import de.uka.ilkd.key.strategy.IBreakpointStopCondition;
 import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint;
 
 import org.key_project.prover.engine.SingleRuleApplicationInfo;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/CompoundStopCondition.java

@@ -10,11 +10,11 @@
 
 import de.uka.ilkd.key.proof.Goal;
 
+import org.jspecify.annotations.NullMarked;
 import org.key_project.prover.engine.SingleRuleApplicationInfo;
 import org.key_project.prover.engine.StopCondition;
 
 import org.jspecify.annotations.NonNull;
-import org.jspecify.annotations.NullMarked;
 import org.jspecify.annotations.Nullable;
 
 /**
@@ -44,6 +44,9 @@ public class CompoundStopCondition implements StopCondition<Goal> {
      */
     private @Nullable StopCondition<Goal> lastShouldStopChild;
 
+    public CompoundStopCondition() {
+    }
+
     /**
      * Constructor.
      *

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/strategy/IBreakpointStopCondition.java → key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/IBreakpointStopCondition.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.strategy;
+package de.uka.ilkd.key.symbolic_execution.strategy;
 
 import java.util.Set;
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionBreakpointStopCondition.java

@@ -13,7 +13,6 @@
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.NodeInfo;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.strategy.IBreakpointStopCondition;
 import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint;
 
 import org.key_project.prover.rules.RuleApp;

key.core.symbolic_execution/src/main/java/module-info.java

@@ -0,0 +1,31 @@
+import de.uka.ilkd.key.proof.init.POExtension;
+import de.uka.ilkd.key.symbolic_execution.po.TruthValuePOExtension;
+
+import org.jspecify.annotations.NullMarked;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (31.03.24)
+ */
+@NullMarked module key.core.symbolic_execution {
+    exports de.uka.ilkd.key.symbolic_execution;
+    exports de.uka.ilkd.key.symbolic_execution.model;
+    exports de.uka.ilkd.key.symbolic_execution.po;
+    exports de.uka.ilkd.key.symbolic_execution.profile;
+    exports de.uka.ilkd.key.symbolic_execution.strategy;
+    exports de.uka.ilkd.key.symbolic_execution.strategy.breakpoint;
+    exports de.uka.ilkd.key.symbolic_execution.util;
+
+    requires java.xml;
+    requires key.core;
+    requires key.ncore;
+    requires org.key_project.util;
+    requires java.desktop;
+    requires org.slf4j;
+    requires org.jspecify;
+    requires key.prover;
+    requires org.checkerframework.checker.qual;
+
+    provides POExtension with TruthValuePOExtension;
+}

key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java

@@ -20,7 +20,6 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.proof.TermProgramVariableCollectorKeepUpdatesForBreakpointconditions;
 import de.uka.ilkd.key.proof.init.FunctionalOperationContractPO;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.proof.init.ProofOblInput;
@@ -39,6 +38,7 @@
 import de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO;
 import de.uka.ilkd.key.symbolic_execution.po.ProgramMethodSubsetPO;
 import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfile;
+import de.uka.ilkd.key.symbolic_execution.proof.TermProgramVariableCollectorKeepUpdatesForBreakpointconditions;
 import de.uka.ilkd.key.symbolic_execution.strategy.*;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;