module-info.java, 2nd attempt

build.gradle

@@ -59,6 +59,12 @@ subprojects {
 
     repositories {
         mavenCentral()
+        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 {

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.infflow/src/main/java/module-info.java

@@ -0,0 +1,15 @@
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (3/22/26)
+ */
+module key.core.infflow {
+    exports de.uka.ilkd.key.informationflow.macros;
+    exports de.uka.ilkd.key.informationflow.impl;
+    requires key.core;
+    requires key.ncore;
+    requires key.prover;
+    requires org.jspecify;
+    requires org.key_project.util;
+    requires org.slf4j;
+}

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;