Skip to content

Commit 39eed3f

Browse files
wadoonwadoon
committed
Make package unique and sealable.
1 parent 2fb07b6 commit 39eed3f

File tree

344 files changed

+1032
-1159
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

344 files changed

+1032
-1159
lines changed

‎build.gradle‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -79,9 +79,12 @@ subprojects {
7979

8080
repositories {
8181
mavenCentral()
82-
maven {
82+
maven { // cleary if needed?!
8383
url 'https://git.key-project.org/api/v4/projects/35/packages/maven'
8484
}
85+
maven { // remove if docking frames 1.1.3p2 on Maven Central
86+
url "https://s01.oss.sonatype.org/content/repositories/snapshots/"
87+
}
8588
}
8689

8790
dependencies {

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

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -17,18 +17,18 @@
1717
import de.uka.ilkd.key.proof.init.AbstractOperationPO;
1818
import de.uka.ilkd.key.settings.ChoiceSettings;
1919
import de.uka.ilkd.key.settings.ProofSettings;
20-
import de.uka.ilkd.key.symbolic_execution.ExecutionNodePreorderIterator;
21-
import de.uka.ilkd.key.symbolic_execution.SymbolicExecutionTreeBuilder;
22-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
23-
import de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO;
24-
import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfile;
25-
import de.uka.ilkd.key.symbolic_execution.strategy.CompoundStopCondition;
26-
import de.uka.ilkd.key.symbolic_execution.strategy.ExecutedSymbolicExecutionTreeNodesStopCondition;
27-
import de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionBreakpointStopCondition;
28-
import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.ExceptionBreakpoint;
29-
import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint;
30-
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment;
31-
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
20+
import de.uka.ilkd.key.symbex.ExecutionNodePreorderIterator;
21+
import de.uka.ilkd.key.symbex.SymbolicExecutionTreeBuilder;
22+
import de.uka.ilkd.key.symbex.model.IExecutionNode;
23+
import de.uka.ilkd.key.symbex.po.ProgramMethodPO;
24+
import de.uka.ilkd.key.symbex.profile.SymbolicExecutionJavaProfile;
25+
import de.uka.ilkd.key.symbex.strategy.CompoundStopCondition;
26+
import de.uka.ilkd.key.symbex.strategy.ExecutedSymbolicExecutionTreeNodesStopCondition;
27+
import de.uka.ilkd.key.symbex.strategy.SymbolicExecutionBreakpointStopCondition;
28+
import de.uka.ilkd.key.symbex.strategy.breakpoint.ExceptionBreakpoint;
29+
import de.uka.ilkd.key.symbex.strategy.breakpoint.IBreakpoint;
30+
import de.uka.ilkd.key.symbex.util.SymbolicExecutionEnvironment;
31+
import de.uka.ilkd.key.symbex.util.SymbolicExecutionUtil;
3232
import de.uka.ilkd.key.util.MiscTools;
3333

3434
import org.key_project.util.collection.ImmutableSLList;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java renamed to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbex/AbstractUpdateExtractor.java

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
package de.uka.ilkd.key.symbolic_execution;
4+
package de.uka.ilkd.key.symbex;
55

66
import java.util.*;
77
import java.util.Map.Entry;
@@ -20,10 +20,10 @@
2020
import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
2121
import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo;
2222
import de.uka.ilkd.key.strategy.StrategyProperties;
23-
import de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionAllArrayIndicesVariable;
24-
import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicLayout;
25-
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
26-
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
23+
import de.uka.ilkd.key.symbex.model.impl.ExecutionAllArrayIndicesVariable;
24+
import de.uka.ilkd.key.symbex.object_model.ISymbolicLayout;
25+
import de.uka.ilkd.key.symbex.util.SymbolicExecutionSideProofUtil;
26+
import de.uka.ilkd.key.symbex.util.SymbolicExecutionUtil;
2727

2828
import org.key_project.logic.Name;
2929
import org.key_project.logic.sort.Sort;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractWriter.java renamed to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbex/AbstractWriter.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
package de.uka.ilkd.key.symbolic_execution;
4+
package de.uka.ilkd.key.symbex;
55

66
import java.util.Map;
77
import java.util.Map.Entry;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodePreorderIterator.java renamed to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbex/ExecutionNodePreorderIterator.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
package de.uka.ilkd.key.symbolic_execution;
4+
package de.uka.ilkd.key.symbex;
55

6-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
6+
import de.uka.ilkd.key.symbex.model.IExecutionNode;
77

88
/**
99
* <p>

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java renamed to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbex/ExecutionNodeReader.java

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
package de.uka.ilkd.key.symbolic_execution;
4+
package de.uka.ilkd.key.symbex;
55

66
import java.io.File;
77
import java.io.FileInputStream;
@@ -29,10 +29,10 @@
2929
import de.uka.ilkd.key.speclang.BlockContract;
3030
import de.uka.ilkd.key.speclang.Contract;
3131
import de.uka.ilkd.key.speclang.LoopSpecification;
32-
import de.uka.ilkd.key.symbolic_execution.model.*;
33-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionTermination.TerminationKind;
34-
import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicEquivalenceClass;
35-
import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicLayout;
32+
import de.uka.ilkd.key.symbex.model.*;
33+
import de.uka.ilkd.key.symbex.model.IExecutionTermination.TerminationKind;
34+
import de.uka.ilkd.key.symbex.object_model.ISymbolicEquivalenceClass;
35+
import de.uka.ilkd.key.symbex.object_model.ISymbolicLayout;
3636

3737
import org.key_project.logic.sort.Sort;
3838
import org.key_project.util.collection.ImmutableList;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeSymbolicLayoutExtractor.java renamed to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbex/ExecutionNodeSymbolicLayoutExtractor.java

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
package de.uka.ilkd.key.symbolic_execution;
4+
package de.uka.ilkd.key.symbex;
55

66
import de.uka.ilkd.key.proof.init.ProofInputException;
7-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
8-
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
7+
import de.uka.ilkd.key.symbex.model.IExecutionNode;
8+
import de.uka.ilkd.key.symbex.util.SymbolicExecutionUtil;
99

1010
/**
1111
* Special {@link SymbolicLayoutExtractor} for {@link IExecutionNode}s.

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeWriter.java renamed to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbex/ExecutionNodeWriter.java

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
package de.uka.ilkd.key.symbolic_execution;
4+
package de.uka.ilkd.key.symbex;
55

66
import java.io.File;
77
import java.io.FileOutputStream;
@@ -12,29 +12,29 @@
1212
import java.util.Map;
1313

1414
import de.uka.ilkd.key.proof.init.ProofInputException;
15-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionAuxiliaryContract;
16-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionBaseMethodReturn;
17-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionBlockStartNode;
18-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionBranchCondition;
19-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionBranchStatement;
20-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionConstraint;
21-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionElement;
22-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionExceptionalMethodReturn;
23-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionJoin;
24-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionLink;
25-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionLoopCondition;
26-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionLoopInvariant;
27-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionLoopStatement;
28-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionMethodCall;
29-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionMethodReturn;
30-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionMethodReturnValue;
31-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
32-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionOperationContract;
33-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionStart;
34-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionStatement;
35-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionTermination;
36-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionValue;
37-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionVariable;
15+
import de.uka.ilkd.key.symbex.model.IExecutionAuxiliaryContract;
16+
import de.uka.ilkd.key.symbex.model.IExecutionBaseMethodReturn;
17+
import de.uka.ilkd.key.symbex.model.IExecutionBlockStartNode;
18+
import de.uka.ilkd.key.symbex.model.IExecutionBranchCondition;
19+
import de.uka.ilkd.key.symbex.model.IExecutionBranchStatement;
20+
import de.uka.ilkd.key.symbex.model.IExecutionConstraint;
21+
import de.uka.ilkd.key.symbex.model.IExecutionElement;
22+
import de.uka.ilkd.key.symbex.model.IExecutionExceptionalMethodReturn;
23+
import de.uka.ilkd.key.symbex.model.IExecutionJoin;
24+
import de.uka.ilkd.key.symbex.model.IExecutionLink;
25+
import de.uka.ilkd.key.symbex.model.IExecutionLoopCondition;
26+
import de.uka.ilkd.key.symbex.model.IExecutionLoopInvariant;
27+
import de.uka.ilkd.key.symbex.model.IExecutionLoopStatement;
28+
import de.uka.ilkd.key.symbex.model.IExecutionMethodCall;
29+
import de.uka.ilkd.key.symbex.model.IExecutionMethodReturn;
30+
import de.uka.ilkd.key.symbex.model.IExecutionMethodReturnValue;
31+
import de.uka.ilkd.key.symbex.model.IExecutionNode;
32+
import de.uka.ilkd.key.symbex.model.IExecutionOperationContract;
33+
import de.uka.ilkd.key.symbex.model.IExecutionStart;
34+
import de.uka.ilkd.key.symbex.model.IExecutionStatement;
35+
import de.uka.ilkd.key.symbex.model.IExecutionTermination;
36+
import de.uka.ilkd.key.symbex.model.IExecutionValue;
37+
import de.uka.ilkd.key.symbex.model.IExecutionVariable;
3838
import de.uka.ilkd.key.util.LinkedHashMap;
3939

4040
import org.key_project.util.collection.ImmutableList;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionVariableExtractor.java renamed to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbex/ExecutionVariableExtractor.java

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
package de.uka.ilkd.key.symbolic_execution;
4+
package de.uka.ilkd.key.symbex;
55

66
import java.util.*;
77

@@ -12,13 +12,13 @@
1212
import de.uka.ilkd.key.logic.op.ProgramVariable;
1313
import de.uka.ilkd.key.proof.Node;
1414
import de.uka.ilkd.key.proof.init.ProofInputException;
15-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionConstraint;
16-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
17-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionValue;
18-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionVariable;
19-
import de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionValue;
20-
import de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionVariable;
21-
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
15+
import de.uka.ilkd.key.symbex.model.IExecutionConstraint;
16+
import de.uka.ilkd.key.symbex.model.IExecutionNode;
17+
import de.uka.ilkd.key.symbex.model.IExecutionValue;
18+
import de.uka.ilkd.key.symbex.model.IExecutionVariable;
19+
import de.uka.ilkd.key.symbex.model.impl.AbstractExecutionValue;
20+
import de.uka.ilkd.key.symbex.model.impl.AbstractExecutionVariable;
21+
import de.uka.ilkd.key.symbex.util.SymbolicExecutionUtil;
2222

2323
import org.key_project.util.collection.ImmutableList;
2424
import org.key_project.util.collection.ImmutableSLList;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java renamed to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbex/SymbolicExecutionTreeBuilder.java

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/* This file is part of KeY - https://key-project.org
22
* KeY is licensed under the GNU General Public License Version 2
33
* SPDX-License-Identifier: GPL-2.0-only */
4-
package de.uka.ilkd.key.symbolic_execution;
4+
package de.uka.ilkd.key.symbex;
55

66
import java.util.*;
77
import java.util.Map.Entry;
@@ -27,13 +27,13 @@
2727
import de.uka.ilkd.key.rule.WhileInvariantRule;
2828
import de.uka.ilkd.key.rule.merge.MergePartner;
2929
import de.uka.ilkd.key.rule.merge.MergeRuleBuiltInRuleApp;
30-
import de.uka.ilkd.key.symbolic_execution.model.*;
31-
import de.uka.ilkd.key.symbolic_execution.model.IExecutionTermination.TerminationKind;
32-
import de.uka.ilkd.key.symbolic_execution.model.impl.*;
33-
import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfile;
34-
import de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionStrategy;
35-
import de.uka.ilkd.key.symbolic_execution.util.DefaultEntry;
36-
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
30+
import de.uka.ilkd.key.symbex.model.*;
31+
import de.uka.ilkd.key.symbex.model.IExecutionTermination.TerminationKind;
32+
import de.uka.ilkd.key.symbex.model.impl.*;
33+
import de.uka.ilkd.key.symbex.profile.SymbolicExecutionJavaProfile;
34+
import de.uka.ilkd.key.symbex.strategy.SymbolicExecutionStrategy;
35+
import de.uka.ilkd.key.symbex.util.DefaultEntry;
36+
import de.uka.ilkd.key.symbex.util.SymbolicExecutionUtil;
3737
import de.uka.ilkd.key.util.MiscTools;
3838
import de.uka.ilkd.key.util.NodePreorderIterator;
3939

0 commit comments

Comments
 (0)