names) {}
+
private static Name makeUnique(Name name, Goal goal) {
+ var used = goal.proof().lookup(InfFlowUsedTacletNames.class);
+ if(used == null) {
+ used = new InfFlowUsedTacletNames(new TreeSet<>());
+ goal.proof().register(used, InfFlowUsedTacletNames.class);
+ }
+
int i = 0;
- final String s = name.toString();
- name = new Name(s + "_" + getBranchUID(goal.node()));
- while (InfFlowContractAppTaclet.registered(name)) {
- name = new Name(s + "_" + i++);
+ var base = name.toString() + "_" + getBranchUID(goal.node());
+ var s = base;
+ while (used.names.contains(s)) {
+ s = s + "_" + i++;
}
- InfFlowContractAppTaclet.register(name);
+ used.names.add(base);
return name;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java
similarity index 100%
rename from key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java
rename to key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java
similarity index 99%
rename from key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java
rename to key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java
index 8819910e37b..2407deff6c5 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java
+++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java
@@ -6,6 +6,7 @@
import java.util.Iterator;
import java.util.Map;
+import de.uka.ilkd.key.informationflow.ProofObligationVars;
import de.uka.ilkd.key.informationflow.po.IFProofObligationVars;
import de.uka.ilkd.key.informationflow.proof.init.StateVars;
import de.uka.ilkd.key.java.Services;
@@ -13,7 +14,6 @@
import de.uka.ilkd.key.logic.label.TermLabelManager;
import de.uka.ilkd.key.logic.op.VariableSV;
import de.uka.ilkd.key.proof.OpReplacer;
-import de.uka.ilkd.key.proof.init.ProofObligationVars;
import de.uka.ilkd.key.rule.RewriteTaclet;
import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletBuilder;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/BlockInfFlowUnfoldTacletBuilder.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/BlockInfFlowUnfoldTacletBuilder.java
similarity index 100%
rename from key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/BlockInfFlowUnfoldTacletBuilder.java
rename to key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/BlockInfFlowUnfoldTacletBuilder.java
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowBlockContractTacletBuilder.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowBlockContractTacletBuilder.java
similarity index 98%
rename from key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowBlockContractTacletBuilder.java
rename to key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowBlockContractTacletBuilder.java
index c25cef0b7dc..2cee8aa8cdc 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowBlockContractTacletBuilder.java
+++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowBlockContractTacletBuilder.java
@@ -3,13 +3,13 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.informationflow.rule.tacletbuilder;
+import de.uka.ilkd.key.informationflow.ProofObligationVars;
import de.uka.ilkd.key.informationflow.po.snippet.BasicPOSnippetFactory;
import de.uka.ilkd.key.informationflow.po.snippet.InfFlowPOSnippetFactory;
import de.uka.ilkd.key.informationflow.po.snippet.POSnippetFactory;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.reference.ExecutionContext;
import de.uka.ilkd.key.logic.JTerm;
-import de.uka.ilkd.key.proof.init.ProofObligationVars;
import de.uka.ilkd.key.speclang.BlockContract;
import de.uka.ilkd.key.util.MiscTools;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowLoopInvariantTacletBuilder.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowLoopInvariantTacletBuilder.java
similarity index 98%
rename from key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowLoopInvariantTacletBuilder.java
rename to key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowLoopInvariantTacletBuilder.java
index d61e2a069a2..81390f481c1 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowLoopInvariantTacletBuilder.java
+++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowLoopInvariantTacletBuilder.java
@@ -3,13 +3,13 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.informationflow.rule.tacletbuilder;
+import de.uka.ilkd.key.informationflow.ProofObligationVars;
import de.uka.ilkd.key.informationflow.po.snippet.BasicPOSnippetFactory;
import de.uka.ilkd.key.informationflow.po.snippet.InfFlowPOSnippetFactory;
import de.uka.ilkd.key.informationflow.po.snippet.POSnippetFactory;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.reference.ExecutionContext;
import de.uka.ilkd.key.logic.JTerm;
-import de.uka.ilkd.key.proof.init.ProofObligationVars;
import de.uka.ilkd.key.speclang.LoopSpecification;
import de.uka.ilkd.key.util.MiscTools;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowMethodContractTacletBuilder.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowMethodContractTacletBuilder.java
similarity index 96%
rename from key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowMethodContractTacletBuilder.java
rename to key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowMethodContractTacletBuilder.java
index 79dd351d0bc..8066f6c1d59 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowMethodContractTacletBuilder.java
+++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowMethodContractTacletBuilder.java
@@ -3,16 +3,16 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.informationflow.rule.tacletbuilder;
+import de.uka.ilkd.key.informationflow.ProofObligationVars;
import de.uka.ilkd.key.informationflow.po.snippet.BasicPOSnippetFactory;
import de.uka.ilkd.key.informationflow.po.snippet.InfFlowPOSnippetFactory;
import de.uka.ilkd.key.informationflow.po.snippet.POSnippetFactory;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.JTerm;
import de.uka.ilkd.key.logic.op.IProgramMethod;
-import de.uka.ilkd.key.proof.init.ProofObligationVars;
import de.uka.ilkd.key.speclang.Contract;
import de.uka.ilkd.key.speclang.FunctionalOperationContract;
-import de.uka.ilkd.key.speclang.InformationFlowContract;
+import de.uka.ilkd.key.speclang.infflow.InformationFlowContract;
import de.uka.ilkd.key.util.MiscTools;
import org.key_project.logic.Name;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/LoopInfFlowUnfoldTacletBuilder.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/LoopInfFlowUnfoldTacletBuilder.java
similarity index 100%
rename from key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/LoopInfFlowUnfoldTacletBuilder.java
rename to key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/LoopInfFlowUnfoldTacletBuilder.java
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/MethodInfFlowUnfoldTacletBuilder.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/MethodInfFlowUnfoldTacletBuilder.java
similarity index 95%
rename from key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/MethodInfFlowUnfoldTacletBuilder.java
rename to key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/MethodInfFlowUnfoldTacletBuilder.java
index 27d2dbe459a..f6c7a4ef33b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/MethodInfFlowUnfoldTacletBuilder.java
+++ b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/MethodInfFlowUnfoldTacletBuilder.java
@@ -8,7 +8,7 @@
import de.uka.ilkd.key.informationflow.po.snippet.POSnippetFactory;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.JTerm;
-import de.uka.ilkd.key.speclang.InformationFlowContract;
+import de.uka.ilkd.key.speclang.infflow.InformationFlowContract;
import de.uka.ilkd.key.util.MiscTools;
import org.key_project.logic.Name;
diff --git a/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro b/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro
new file mode 100644
index 00000000000..47630a79864
--- /dev/null
+++ b/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro
@@ -0,0 +1,14 @@
+#
+# Macros to appear in the context menu
+# (this list is loaded into ProofMacroMenu#REGISTERED_MACROS)
+#
+# warning: subject to change of package name
+
+
+de.uka.ilkd.key.informationflow.macros.FullInformationFlowAutoPilotMacro
+de.uka.ilkd.key.informationflow.macros.AuxiliaryComputationAutoPilotMacro
+de.uka.ilkd.key.informationflow.macros.StartAuxiliaryComputationMacro
+de.uka.ilkd.key.informationflow.macros.FinishAuxiliaryComputationMacro
+de.uka.ilkd.key.informationflow.macros.StateExpansionAndInfFlowContractApplicationMacro
+de.uka.ilkd.key.informationflow.macros.SelfcompositionStateExpansionMacro
+de.uka.ilkd.key.informationflow.macros.FullUseInformationFlowContractMacro
\ No newline at end of file
diff --git a/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver b/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver
new file mode 100644
index 00000000000..28da98730d2
--- /dev/null
+++ b/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver
@@ -0,0 +1 @@
+de.uka.ilkd.key.informationflow.InfFlowProfileResolver
diff --git a/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.loader.ProofObligationLoader b/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.loader.ProofObligationLoader
new file mode 100644
index 00000000000..d0f7fe1fef3
--- /dev/null
+++ b/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.loader.ProofObligationLoader
@@ -0,0 +1 @@
+de.uka.ilkd.key.informationflow.po.InfFlowContractPOLoader
diff --git a/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.speclang.infflow.InformationFlowContractSupplier b/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.speclang.infflow.InformationFlowContractSupplier
new file mode 100644
index 00000000000..c714cf54cdf
--- /dev/null
+++ b/key.core.infflow/src/main/resources/META-INF/services/de.uka.ilkd.key.speclang.infflow.InformationFlowContractSupplier
@@ -0,0 +1 @@
+de.uka.ilkd.key.informationflow.impl.InformationFlowContractImplSupplier
\ No newline at end of file
diff --git a/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/GenerateUnitTests.java b/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/GenerateUnitTests.java
new file mode 100644
index 00000000000..42c0bfe73ef
--- /dev/null
+++ b/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/GenerateUnitTests.java
@@ -0,0 +1,41 @@
+/* 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.informationflow;
+
+import java.io.IOException;
+import java.nio.file.Paths;
+import java.util.*;
+
+import de.uka.ilkd.key.proof.runallproofs.ProofCollections;
+
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import static de.uka.ilkd.key.proof.runallproofs.GenerateUnitTests.*;
+
+/**
+ * Generation of test cases (JUnit) for given proof collection files.
+ *
+ * This class is intended to be called from gradle. See the gradle task
+ * {@code generateRunAllProofs}.
+ *
+ * The considered proof collections files are configured statically in
+ * {@link ProofCollections}.
+ *
+ * @author Alexander Weigl
+ * @version 1 (6/14/20)
+ */
+public class GenerateUnitTests {
+ private static final Logger LOGGER = LoggerFactory.getLogger(GenerateUnitTests.class);
+
+ public static void main(String[] args) throws IOException {
+ var collections = List.of(InfFlowProofCollection.automaticInfFlow());
+ if (args.length != 1) {
+ System.err.println("Usage: ");
+ System.exit(1);
+ }
+ var outputFolder = Paths.get(args[0]);
+ run(outputFolder, collections);
+ }
+}
diff --git a/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/InfFlowProofCollection.java b/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/InfFlowProofCollection.java
new file mode 100644
index 00000000000..ce62c3859ac
--- /dev/null
+++ b/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/InfFlowProofCollection.java
@@ -0,0 +1,1047 @@
+/* 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.informationflow;
+
+import java.io.IOException;
+import java.util.Date;
+
+import de.uka.ilkd.key.proof.runallproofs.proofcollection.ForkMode;
+import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollection;
+import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollectionSettings;
+
+import static org.assertj.core.api.Assertions.assertThat;
+
+public class InfFlowProofCollection {
+ public static ProofCollection automaticInfFlow() throws IOException {
+ var settings = new ProofCollectionSettings(new Date());
+ var c = new ProofCollection(settings);
+ /*
+ * Defines a base directory.
+ * All paths in this file are treated relative to base directory (except path for base
+ * directory itself).
+ */
+ settings.setBaseDirectory("../key.ui/examples/InformationFlow/");
+
+ /*
+ * Defines a statistics file.
+ * Path is relative to base directory.
+ */
+ settings.setStatisticsFile(
+ "build/reports/runallproofs/runStatistics_infflow.csv");
+
+ /*
+ * Fork mode setting, can be declared to create subprocesses while running tests declared in
+ * this file.
+ * Possible modes: noFork-all files are proven within a single process
+ * perg = c.group("- one subprocess is created for each group
+ * perFile-one subprocess is created for each file
+ */
+ settings.setForkMode(ForkMode.NOFORK);
+
+ /*
+ * Enable or disable proof reloading.
+ * If enabled, closed proofs will be saved and reloaded after prover is finished.
+ */
+ settings.setReloadEnabled(false);
+
+ /*
+ * Temporary directory, which is used for inter process communication when using forked
+ * mode.
+ * The given path is relative to baseDirectory.
+ */
+ settings.setTempDir("build/runallproofs_infflow_tmp");
+
+ /*
+ * If the fork mode is not set to noFork, the launched subprocesses are terminated as
+ * soon as the timeout specified here has elapsed. No timeout occurs if not specified.
+ *
+ * Timeout per subprocess in seconds
+ */
+ settings.setForkTimeout(1000);
+
+ /*
+ * If the fork mode is not set to noFork, the launched subprocesses
+ * get the specified amount of heap memory.
+ *
+ * Heap memory for subprocesses (like 500m or 2G)
+ */
+ // forkMemory = 1000m
+
+ /*
+ * By default runAllProofs does not print a lot of information.
+ * Set this to true to get more output.
+ */
+ settings.setVerboseOutput(true);
+
+ /*
+ * By default, runAllProofs runs all groups in this file.
+ * By naming a comma separated list of groups here, the
+ * test can be restricted to these groups (for debugging).
+ */
+ // runOnlyOn = group1, group2 (the space after each comma is mandatory)
+ // settings.setRunOnlyOn("performance, performancePOConstruction");
+
+
+ // // Tests for information flow
+
+ var g = c.group("ToyVoting");
+ g.provable(
+ "ToyVoting/Voter(Voter__insecure_voting()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyVoting/Voter(Voter__publishVoterParticipation()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyVoting/Voter(Voter__isValid(int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyVoting/Voter(Voter__sendVote(int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyVoting/Voter(Voter__inputVote()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyVoting/Voter(Voter__secure_voting()).JML normal_behavior operation contract.0.key");
+
+
+ g = c.group("ConditionalConfidential");
+ g.provable(
+ "ConditionalConfidential/CCExample(CCExample__hasAccessRight(CCExample.User)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ConditionalConfidential/CCExample(CCExample__getConfidentialData(CCExample.User)).JML normal_behavior operation contract.0.key");
+
+
+ g = c.group("SumExample");
+ g.provable(
+ "Sum/SumExample(SumExample__getSum()).JML normal_behavior operation contract.0.key");
+
+
+ g = c.group("ToyBanking");
+ g.provable(
+ "ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example.UserAccount(java.lang.Object___inv_()).JML accessible clause.0.key");
+ g.provable(
+ "ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).JML normal_behavior operation contract.0.key");
+
+ g.provable(
+ "ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).JML normal_behavior operation contract.0.key");
+ g.notprovable(
+ "ToyBanking/banking_example2.UserAccount(java.lang.Object___inv_()).JML accessible clause.0.key");
+ g.provable(
+ "ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example2.Bank(banking_example2.Bank__login(int,(C)).JML normal_behavior operation contract.0.key");
+
+
+ g = c.group("BlockContracts");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).JML operation contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).JML operation contract.0.key");
+
+
+ g = c.group("MethodContracts");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param_helper()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n9()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).JML operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).JML operation contract.0.key");
+
+
+ g = c.group("LoopInvariants");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).JML operation contract.0.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).JML operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).JML normal_behavior operation contract.0.key");
+
+
+ g = c.group("MiniExamples");
+ g.provable(
+ "MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).JML operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).JML normal_behavior operation contract.1.key");
+ g.provable(
+ "MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).JML operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).JML normal_behavior operation contract.1.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).JML normal_behavior operation contract.0.key");
+
+
+ g = c.group("NewObjects");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).JML normal_behavior operation contract.1.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).JML operation contract.1.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).JML operation contract.1.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).JML operation contract.0.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).JML accessible clause.0.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).JML normal_behavior operation contract.0.key");
+
+
+ g.notprovable(
+ "PasswordFile/passwordfile.SecurePasswordFile(passwordfile.SecurePasswordFile___userIndex()).JML accessible clause.0.key");
+
+ g = c.group("SimpleEvoting");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage((B)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).JML normal_behavior operation contract.0.key");
+ g.notprovable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).JML normal_behavior operation contract.0.key");
+ g.notprovable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment___rep()).JML accessible clause.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).JML normal_behavior operation contract.1.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Message(java.lang.Object___inv_()).JML accessible clause.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Server(simple_evoting.Server__resultReady()).JML accessible clause.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Server(simple_evoting.Server__resultReady()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onSendResult()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onCollectBallot(simple_evoting.Message)).JML normal_behavior operation contract.1.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Server(simple_evoting.Server__onCollectBallot(simple_evoting.Message)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Server(java.lang.Object___inv_()).JML accessible clause.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__publishResult()).JML normal_behavior operation contract.0.key");
+ g.notprovable(
+ "SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__main()).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Setup(java.lang.Object___inv_()).JML accessible clause.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).JML normal_behavior operation contract.1.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).JML normal_behavior operation contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Voter(java.lang.Object___inv_()).JML accessible clause.0.key");
+
+
+ // // Tests for information flow to be executed without information flow proof macro
+ // c = new ProofCollection(settings);
+
+ g = c.group("ToyVoting_nomacro");
+ g.notprovable("ToyVoting/Voter(Voter__insecure_voting()).Non-interference contract.0.key");
+ g.provable(
+ "ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.key");
+ g.provable("ToyVoting/Voter(Voter__isValid(int)).Non-interference contract.0.key");
+ g.provable("ToyVoting/Voter(Voter__sendVote(int)).Non-interference contract.0.key");
+ g.provable("ToyVoting/Voter(Voter__inputVote()).Non-interference contract.0.key");
+ // g.provable("ToyVoting/Voter(Voter__secure_voting()).Non-interference contract.0.key");
+
+
+ g = c.group("ConditionalConfidential_nomacro");
+ // g.provable("ConditionalConfidential/CCExample(CCExample__getConfidentialData(CCExample.User)).Non-interference
+ // contract.0.key");
+
+
+ g = c.group("SumExample_nomacro");
+ g.provable("Sum/SumExample(SumExample__getSum()).Non-interference contract.0.key");
+
+
+ g = c.group("ToyBanking_nomacro");
+ g.provable(
+ "ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.key");
+ // g.provable("ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).Non-interference
+ // contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).Non-interference contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).Non-interference contract.0.key");
+ g.notprovable(
+ "ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).Non-interference contract.0.key");
+ // g.provable("ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).Non-interference
+ // contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).Non-interference contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).Non-interference contract.0.key");
+ g.provable(
+ "ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).Non-interference contract.0.key");
+ // g.provable("ToyBanking/banking_example2.Bank(banking_example2.Bank__login(int,(C)).Non-interference
+ // contract.0.key");
+
+
+ g = c.group("BlockContracts_nomacro");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.key");
+ g.provable(
+ "BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).Non-interference contract.0.key");
+
+
+ g = c.group("MethodContracts_nomacro");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).Non-interference contract.0.key");
+ g.notprovable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).Non-interference contract.0.key");
+ g.notprovable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).Non-interference contract.0.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).Non-interference contract.0.key");
+
+
+ g = c.group("LoopInvariants_nomacro");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).Non-interference contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).Non-interference contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).Non-interference contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).Non-interference contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).Non-interference contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).Non-interference contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).Non-interference contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).Non-interference contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).Non-interference contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).Non-interference contract.0.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).Non-interference contract.0.key");
+
+
+ g = c.group("MiniExamples_nomacro");
+ g.notprovable(
+ "MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).Non-interference contract.0.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).Non-interference contract.0.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).Non-interference contract.0.key");
+ g.notprovable(
+ "MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.1.key");
+ g.notprovable(
+ "MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).Non-interference contract.0.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).Non-interference contract.0.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).Non-interference contract.0.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.1.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.0.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).Non-interference contract.0.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).Non-interference contract.0.key");
+
+
+ g = c.group("NewObjects_nomacro");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).Non-interference contract.0.key");
+ g.notprovable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.1.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.0.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).Non-interference contract.0.key");
+ // g.provable("NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).Non-interference
+ // contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).Non-interference contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).Non-interference contract.0.key");
+ g.notprovable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.1.key");
+ // g.provable("NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference
+ // contract.0.key");
+ // g.provable("NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).Non-interference
+ // contract.0.key");
+ g.notprovable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).Non-interference contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).Non-interference contract.0.key");
+ g.notprovable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.1.key");
+ g.notprovable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).Non-interference contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).Non-interference contract.0.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).Non-interference contract.0.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).Non-interference contract.0.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).Non-interference contract.0.key");
+
+
+ g = c.group("SimpleEvoting_nomacro");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.key");
+ // g.provable("SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage((B)).Non-interference
+ // contract.0.key");
+ // g.provable("SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).Non-interference
+ // contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.key");
+ g.notprovable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.1.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.0.key");
+ // g.provable("SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).Non-interference
+ // contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).Non-interference contract.0.key");
+ // g.provable("SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__publishResult()).Non-interference
+ // contract.0.key");
+ // g.provable("SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__main()).Non-interference
+ // contract.0.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.1.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.0.key");
+
+
+ // // Tests for information flow to be executed with information flow proof macro
+ // "FullInformationFlowAutoPilotMacro"
+
+ g = c.group("ToyVoting_fullmacro");
+ g.notprovable(
+ "ToyVoting/Voter(Voter__insecure_voting()).Non-interference contract.0.m.key");
+ g.provable(
+ "ToyVoting/Voter(Voter__publishVoterParticipation()).Non-interference contract.0.m.key");
+ g.provable("ToyVoting/Voter(Voter__isValid(int)).Non-interference contract.0.m.key");
+ g.provable("ToyVoting/Voter(Voter__sendVote(int)).Non-interference contract.0.m.key");
+ g.provable("ToyVoting/Voter(Voter__inputVote()).Non-interference contract.0.m.key");
+ g.provable("ToyVoting/Voter(Voter__secure_voting()).Non-interference contract.0.m.key");
+
+
+ // g.provable("ConditionalConfidential/CCExample(CCExample__getConfidentialData(CCExample.User)).Non-interference
+ // contract.0.m.key");
+
+ g = c.group("SumExample_fullmacro");
+ g.provable("Sum/SumExample(SumExample__getSum()).Non-interference contract.0.m.key");
+
+
+ g = c.group("ToyBanking_fullmacro");
+ g.provable(
+ "ToyBanking/banking_example.UserAccount(banking_example.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "ToyBanking/banking_example.UserAccount(banking_example.UserAccount__tryLogin(int,(C)).Non-interference contract.0.m.key");
+ g.provable(
+ "ToyBanking/banking_example.BankAccount(banking_example.BankAccount__depositMoney(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getBalance()).Non-interference contract.0.m.key");
+ g.provable(
+ "ToyBanking/banking_example.BankAccount(banking_example.BankAccount__getId()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "ToyBanking/banking_example.Bank(banking_example.Bank__login(int,(C)).Non-interference contract.0.m.key");
+ g.provable(
+ "ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__getBankAccount(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "ToyBanking/banking_example2.UserAccount(banking_example2.UserAccount__tryLogin(int,(C)).Non-interference contract.0.m.key");
+ g.provable(
+ "ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__depositMoney(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getBalance()).Non-interference contract.0.m.key");
+ g.provable(
+ "ToyBanking/banking_example2.BankAccount(banking_example2.BankAccount__getId()).Non-interference contract.0.m.key");
+ // g.provable("ToyBanking/banking_example2.Bank(banking_example2.Bank__login(int,(C)).Non-interference
+ // contract.0.m.key");
+
+
+ g = c.group("BlockContracts_fullmacro");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_5()).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_insecure(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__while_block_secure(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_8(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_7(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_6(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithoutBlockContract()).Non-interference contract.0.m.key");
+ g.provable(
+ "BlockContracts/contract.IFEfficiencyExamples(contract.IFEfficiencyExamples__mWithBlockContract()).Non-interference contract.0.m.key");
+
+
+ g = c.group("MethodContracts_fullmacro");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion_2((I,int)).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_recursion(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_catch_exception()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n6()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n6()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_array_param((I,int)).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignment_0_n9()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_if_high_n5_n1()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n5(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n5_n1()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_if_high_n1()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_n5()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n4()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n3()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n3_precond_n4()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__insecure_assignment_n2()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_assignments_n2()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n2()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__n1()).Non-interference contract.0.m.key");
+ g.provable(
+ "MethodContracts/contract.IFMethodContract(contract.IFMethodContract__secure_sequential_n1_n2()).Non-interference contract.0.m.key");
+
+
+ g = c.group("InformationFlow_fullmacro");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_while_3(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_2(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while_4(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile2(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_doubleNestedWhile(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_doubleNestedWhile(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedTwoWhile(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_nestedWhile(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__notSecure_while_wrongInv(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__insecure_twoWhile_2(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_twoWhile(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__loc_secure_while(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__secure_while(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__print(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "LoopInvariants/loop.IFLoopExamples(loop.IFLoopExamples__hammer(int)).Non-interference contract.0.m.key");
+
+ g = c.group("MiniExamples_fullmacro");
+ g.notprovable(
+ "MiniExamples/mini.AliasingExamples(mini.AliasingExamples__insecure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.AliasingExamples(mini.AliasingExamples__secure_1(mini.AliasingExamples,mini.AliasingExamples,int)).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_6()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_5()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_4()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_3()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_2()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamplesLecture(mini.MiniExamplesLecture__m_1()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.1.m.key");
+ g.notprovable(
+ "MiniExamples/mini.DifferenceSeqLocset(mini.DifferenceSeqLocset__m()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_8()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_parameter(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_7()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_2()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_6()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_5()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_4()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_3()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_2()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p2_1()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p2_1()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_6()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_5()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_4()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_3()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_2()).Non-interference contract.0.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.1.m.key");
+ g.provable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__secure_p1_1()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_2()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "MiniExamples/mini.MiniExamples(mini.MiniExamples__insecure_p1_1()).Non-interference contract.0.m.key");
+
+ g = c.group("NewObjects_fullmacro");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee3(object.AmtoftBanerjee3__m()).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_2()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.1.m.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__m_1()).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee(object.AmtoftBanerjee__getQ()).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.Naumann(object.Naumann__Pair_m(int,int)).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_while_i((Ljava.lang.Object)).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_method_call()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.1.m.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__if_two_object_creation_next()).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_if_two_object_creation()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_two_object_creation()).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_two_object_creation()).Non-interference contract.0.m.key");
+ g.notprovable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.1.m.key");
+ g.notprovable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__insecure_object_assignment()).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_3()).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation_2()).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.ObjectOrientation(object.ObjectOrientation__secure_object_creation()).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__expensive(int)).Non-interference contract.0.m.key");
+ g.provable(
+ "NewObjects/object.AmtoftBanerjee2(object.AmtoftBanerjee2__cexp(int)).Non-interference contract.0.m.key");
+
+ g = c.group("SimpleEvoting_fullmacro");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutputMessage((B)).Non-interference contract.0.m.key");
+ // g.provable(
+ // "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage((B)).Non-interference
+ // contract.0.m.key"););
+ g.provable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInputMessage()).Non-interference contract.0.m.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedOutput(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput(int)).Non-interference contract.0.m.key");
+ g.notprovable(
+ "SimpleEvoting/simple_evoting.Environment(simple_evoting.Environment__untrustedInput()).Non-interference contract.0.m.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.1.m.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.SMT(simple_evoting.SMT__send(simple_evoting.Message,int,simple_evoting.Server)).Non-interference contract.0.m.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.SMTEnv(simple_evoting.SMTEnv__send(int,int,int,simple_evoting.Server,int)).Non-interference contract.0.m.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.NetworkClient(simple_evoting.NetworkClient__send((B,simple_evoting.Server,int)).Non-interference contract.0.m.key");
+ // g.provable(
+ // "SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__publishResult()).Non-interference
+ // contract.0.m.key"););
+ // g.provable(
+ // "SimpleEvoting/simple_evoting.Setup(simple_evoting.Setup__main()).Non-interference
+ // contract.0.m.key"););
+ g.provable(
+ "SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.1.m.key");
+ g.provable(
+ "SimpleEvoting/simple_evoting.Voter(simple_evoting.Voter__onSendBallot(simple_evoting.Server)).Non-interference contract.0.m.key");
+
+ for (var testFile : g.getTestFiles()) {
+ try {
+ assertThat(testFile.getKeYFile())
+ .exists()
+ .content().contains("\\profile \"java-infflow\";");
+ } catch (AssertionError e) {
+ System.err.println(testFile.getKeYFile());
+ throw e;
+ }
+ }
+
+ return c;
+ }
+}
diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsInfFlow.java b/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/RunAllProofsInfFlow.java
similarity index 72%
rename from key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsInfFlow.java
rename to key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/RunAllProofsInfFlow.java
index fc48da31a2f..3caeb35ada7 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsInfFlow.java
+++ b/key.core.infflow/src/test/java/de/uka/ilkd/key/informationflow/RunAllProofsInfFlow.java
@@ -1,23 +1,18 @@
/* 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.runallproofs;
+package de.uka.ilkd.key.informationflow;
import java.io.IOException;
import java.util.stream.Stream;
+import de.uka.ilkd.key.proof.runallproofs.RunAllProofsTest;
import de.uka.ilkd.key.proof.runallproofs.proofcollection.StatisticsFile;
import org.junit.jupiter.api.*;
/**
* This test case captures all information flow run-all-proof scenarios.
- *
- * The test case is controlled by the index file (see {@value #INDEX_FILE}).
- *
- * If the property "{@value #SKIP_INF_FLOW_PROPERTY}" is set to true, then no
- * info-flow
- * run-all-proof tests will be run.
*
* @author M. Ulbrich
*/
@@ -27,7 +22,7 @@
public final class RunAllProofsInfFlow {
@TestFactory
Stream data() throws IOException {
- var proofCollection = ProofCollections.automaticInfFlow();
+ var proofCollection = InfFlowProofCollection.automaticInfFlow();
StatisticsFile statisticsFile = proofCollection.getSettings().getStatisticsFile();
statisticsFile.setUp();
Assumptions.assumeTrue(proofCollection != null);
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java
index 516e7904a5c..8305dd144fc 100644
--- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java
+++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionOperationContract.java
@@ -101,23 +101,23 @@ protected String lazyComputeName() throws ProofInputException {
exceptionTerm = search.getExceptionEquality().sub(0);
// Rename variables in contract to the current one
List heapContext =
- HeapContext.getModifiableHeaps(services, inst.transaction);
+ HeapContext.getModifiableHeaps(services, inst.transaction());
Map atPreVars =
UseOperationContractRule.computeAtPreVars(heapContext, services, inst);
Map atPres = HeapContext.getAtPres(atPreVars, services);
LocationVariable baseHeap = services.getTypeConverter().getHeapLDT().getHeap();
JTerm baseHeapTerm = services.getTermBuilder().getBaseHeap();
if (contract.hasSelfVar()) {
- if (inst.pm.isConstructor()) {
+ if (inst.pm().isConstructor()) {
selfTerm = searchConstructorSelfDefinition(search.getWorkingTerm(),
- inst.staticType, services);
+ inst.staticType(), services);
if (selfTerm == null) {
throw new ProofInputException(
"Can't find self term, implementation of UseOperationContractRule might has changed!");
}
KeYJavaType selfType = services.getJavaInfo().getKeYJavaType(selfTerm.sort());
- if (inst.staticType != selfType) {
- throw new ProofInputException("Type \"" + inst.staticType
+ if (inst.staticType() != selfType) {
+ throw new ProofInputException("Type \"" + inst.staticType()
+ "\" expected but found \"" + selfType
+ "\", implementation of UseOperationContractRule might has changed!");
}
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..29ba6cf2c68 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
@@ -91,7 +91,7 @@ public StrategyFactory getDefaultStrategyFactory() {
* {@inheritDoc}
*/
@Override
- public String name() {
+ public String ident() {
return NAME;
}
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..52faa9af592 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
@@ -222,7 +222,7 @@ protected ImmutableList initBuiltInRules() {
* {@inheritDoc}
*/
@Override
- public String name() {
+ public String ident() {
return NAME;
}
diff --git a/key.core.wd/build.gradle b/key.core.wd/build.gradle
new file mode 100644
index 00000000000..cbf92d09e6a
--- /dev/null
+++ b/key.core.wd/build.gradle
@@ -0,0 +1,22 @@
+dependencies {
+ api(project(":key.core"))
+ testImplementation(project(":key.core").sourceSets.test.output)
+}
+
+tasks.register('testRunAllWdProofs', Test) {
+ description = 'Prove/reload all keyfiles tagged for regression testing'
+ group = "verification"
+ filter {
+ includeTestsMatching "RunAllProofsWd"
+ }
+}
+
+
+def rapDir = layout.buildDirectory.dir("generated-src/rap/").getOrNull()
+sourceSets.test.java.srcDirs(rapDir)
+
+tasks.register('generateRAPUnitTests', JavaExec) {
+ classpath = sourceSets.test.runtimeClasspath
+ mainClass.set("de.uka.ilkd.key.wd.GenerateUnitTests")
+ args(rapDir)
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/BlockWellDefinedness.java
similarity index 97%
rename from key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java
rename to key.core.wd/src/main/java/de/uka/ilkd/key/wd/BlockWellDefinedness.java
index 466775d3799..ca129058fc8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/BlockWellDefinedness.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.speclang;
+package de.uka.ilkd.key.wd;
import java.util.function.UnaryOperator;
@@ -13,6 +13,8 @@
import de.uka.ilkd.key.logic.TermServices;
import de.uka.ilkd.key.logic.op.IObserverFunction;
import de.uka.ilkd.key.logic.op.LocationVariable;
+import de.uka.ilkd.key.speclang.BlockContract;
+import de.uka.ilkd.key.speclang.Contract;
import org.key_project.prover.sequent.SequentFormula;
import org.key_project.util.collection.ImmutableSet;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/ClassWellDefinedness.java
similarity index 98%
rename from key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java
rename to key.core.wd/src/main/java/de/uka/ilkd/key/wd/ClassWellDefinedness.java
index 59b3023ccf6..4c0c6572f4a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/ClassWellDefinedness.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.speclang;
+package de.uka.ilkd.key.wd;
import java.util.function.UnaryOperator;
@@ -13,6 +13,7 @@
import de.uka.ilkd.key.logic.TermServices;
import de.uka.ilkd.key.logic.op.*;
import de.uka.ilkd.key.rule.RewriteTaclet;
+import de.uka.ilkd.key.speclang.ClassInvariant;
import org.key_project.logic.Name;
import org.key_project.logic.op.Function;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/LoopWellDefinedness.java
similarity index 97%
rename from key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java
rename to key.core.wd/src/main/java/de/uka/ilkd/key/wd/LoopWellDefinedness.java
index 768a7e9359c..e25fa4cce04 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/LoopWellDefinedness.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.speclang;
+package de.uka.ilkd.key.wd;
import java.util.function.UnaryOperator;
@@ -13,6 +13,8 @@
import de.uka.ilkd.key.logic.TermServices;
import de.uka.ilkd.key.logic.op.IObserverFunction;
import de.uka.ilkd.key.logic.op.LocationVariable;
+import de.uka.ilkd.key.speclang.Contract;
+import de.uka.ilkd.key.speclang.LoopSpecification;
import org.key_project.prover.sequent.SequentFormula;
import org.key_project.util.collection.ImmutableSet;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/MethodWellDefinedness.java
similarity index 99%
rename from key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java
rename to key.core.wd/src/main/java/de/uka/ilkd/key/wd/MethodWellDefinedness.java
index 87b94b36242..82d5ad4c97d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/MethodWellDefinedness.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.speclang;
+package de.uka.ilkd.key.wd;
import java.util.LinkedHashMap;
import java.util.Map;
@@ -16,6 +16,7 @@
import de.uka.ilkd.key.logic.op.*;
import de.uka.ilkd.key.rule.RewriteTaclet;
import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletGoalTemplate;
+import de.uka.ilkd.key.speclang.*;
import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor;
import org.key_project.logic.Name;
diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/SpecificationRepositoryWD.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/SpecificationRepositoryWD.java
new file mode 100644
index 00000000000..598d90ada8c
--- /dev/null
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/SpecificationRepositoryWD.java
@@ -0,0 +1,385 @@
+/* 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.wd;
+
+import java.util.LinkedHashMap;
+import java.util.Map;
+import java.util.Objects;
+import java.util.function.UnaryOperator;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.declaration.modifier.VisibilityModifier;
+import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.logic.op.IObserverFunction;
+import de.uka.ilkd.key.logic.op.ProgramVariable;
+import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+import de.uka.ilkd.key.speclang.*;
+
+import org.key_project.util.collection.*;
+
+import org.jspecify.annotations.NullMarked;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+/**
+ * A special variant of
+ *
+ * @author Alexander Weigl
+ * @version 1 (1/1/26)
+ */
+@NullMarked
+public class SpecificationRepositoryWD extends SpecificationRepository {
+ private static final Logger LOGGER = LoggerFactory.getLogger(SpecificationRepositoryWD.class);
+
+ private final Map, ImmutableSet> wdChecks =
+ new LinkedHashMap<>();
+
+ public SpecificationRepositoryWD(Services services) {
+ super(services);
+ }
+
+ @Override
+ protected void registerContract(Contract contract,
+ Pair targetPair) {
+ LOGGER.trace("Contract registered {}", contract);
+ if (!WellDefinednessCheck.isOn(services) && contract instanceof WellDefinednessCheck) {
+ return;
+ }
+ super.registerContract(contract, targetPair);
+
+ final KeYJavaType targetKJT = targetPair.first;
+ final IObserverFunction targetMethod = targetPair.second;
+
+ if (contract instanceof FunctionalOperationContract) {
+ // Create new well-definedness check
+ final MethodWellDefinedness mwd =
+ new MethodWellDefinedness((FunctionalOperationContract) contract, services);
+ registerContract(mwd, targetPair);
+ } else if (contract instanceof DependencyContract && contract.getOrigVars().atPres.isEmpty()
+ && Objects.equals(targetMethod.getContainerType(),
+ services.getJavaInfo().getJavaLangObject())) {
+ // Create or extend a well-definedness check for a class invariant
+ final JTerm deps =
+ contract.getAccessible(services.getTypeConverter().getHeapLDT().getHeap());
+ final JTerm mby = contract.getMby();
+ final String invName = "JML model class invariant in " + targetKJT.getName();
+ final ClassInvariant inv = new ClassInvariantImpl(invName, invName, targetKJT,
+ contract.getVisibility(), tb.tt(), contract.getOrigVars().self);
+ ClassWellDefinedness cwd =
+ new ClassWellDefinedness(inv, targetMethod, deps, mby, services);
+ final ImmutableSet cwds = getWdClassChecks(targetKJT);
+ if (!cwds.isEmpty()) {
+ assert cwds.size() == 1;
+ final ClassWellDefinedness oldCwd = cwds.iterator().next();
+ unregisterContract(oldCwd);
+ oldCwd.addInv(cwd.getInvariant().getInv(oldCwd.getOrigVars().self, services));
+ cwd = oldCwd.combine(cwd, services);
+ }
+ registerContract(cwd, targetPair);
+ } else if (contract instanceof DependencyContract
+ && contract.getOrigVars().atPres.isEmpty()) {
+ // Create or extend a well-definedness check for a model field
+ MethodWellDefinedness mwd =
+ new MethodWellDefinedness((DependencyContract) contract, services);
+ final ImmutableSet mwds =
+ getWdMethodChecks(targetKJT, targetMethod);
+ if (!mwds.isEmpty()) {
+ assert mwds.size() == 1;
+ final MethodWellDefinedness oldMwd = mwds.iterator().next();
+ unregisterContract(oldMwd);
+ mwd = mwd.combine(oldMwd, services);
+ }
+ registerContract(mwd, targetPair);
+ } else if (contract instanceof WellDefinednessCheck) {
+ registerWdCheck((WellDefinednessCheck) contract);
+ }
+ /*
+ * contractsByName.put(contract.getName(), contract);
+ * final ImmutableSet oldTargets = getContractTargets(targetKJT);
+ * final ImmutableSet newTargets = oldTargets.add(targetMethod);
+ * contractTargets.put(targetKJT, newTargets);
+ */
+ }
+
+
+ /**
+ * Remove well-definedness checks from a given set of contracts
+ *
+ * @param contracts A set of contracts
+ * @return contracts without well-definedness checks
+ */
+ private static ImmutableSet removeWdChecks(ImmutableSet contracts) {
+ ImmutableList result = ImmutableSLList.nil();
+ if (contracts == null) {
+ return contracts;
+ }
+ for (Contract c : contracts) {
+ if (!(c instanceof WellDefinednessCheck)) {
+ result = result.prepend(c);
+ }
+ }
+ return DefaultImmutableSet.fromImmutableList(result);
+ }
+
+ /**
+ * Registers a well-definedness check. It does not take care of its visibility in the proof
+ * management dialog (this is done in {@link #registerContract(Contract, Pair)}).
+ *
+ * @param check The well-definedness check to be registered
+ */
+ private void registerWdCheck(WellDefinednessCheck check) {
+ ImmutableSet checks =
+ getWdChecks(check.getKJT(), check.getTarget()).add(check);
+ wdChecks.put(new Pair<>(check.getKJT(), check.getTarget()), checks);
+ }
+
+ /**
+ * Unregisters a well-definedness check. It does not take care of its visibility in the proof
+ * management dialog.
+ *
+ * @param check The well-definedness check to be unregistered
+ */
+ private void unregisterWdCheck(WellDefinednessCheck check) {
+ wdChecks.put(new Pair<>(check.getKJT(), check.getTarget()),
+ getWdChecks(check.getKJT(), check.getTarget()).remove(check));
+ }
+
+ /**
+ * Returns all registered (atomic) well-definedness checks for the passed kjt.
+ */
+ private ImmutableSet getWdChecks(KeYJavaType kjt) {
+ assert kjt != null;
+ ImmutableSet result = DefaultImmutableSet.nil();
+ for (WellDefinednessCheck ch : getAllWdChecks()) {
+ if (ch.getKJT().equals(kjt)) {
+ result = result.add(ch);
+ }
+ }
+ return result;
+ }
+
+ /**
+ * Returns all registered (atomic) well-definedness checks for the passed target and kjt.
+ */
+ private ImmutableSet getWdChecks(KeYJavaType kjt,
+ IObserverFunction target) {
+ assert kjt != null;
+ assert target != null;
+ target = getCanonicalFormForKJT(target, kjt);
+ final Pair pair = new Pair<>(kjt, target);
+ final ImmutableSet result = wdChecks.get(pair);
+ return result == null ? DefaultImmutableSet.nil() : result;
+ }
+
+ /**
+ * Returns all registered well-definedness checks for method contracts.
+ */
+ private ImmutableSet getAllWdMethodChecks() {
+ ImmutableSet result = DefaultImmutableSet.nil();
+ for (var s : getAllWdChecks()) {
+ if (s instanceof MethodWellDefinedness) {
+ result = result.add((MethodWellDefinedness) s);
+ }
+ }
+ return result;
+ }
+
+ /**
+ * Returns all registered (atomic) well-definedness method checks for the passed kjt.
+ */
+ private ImmutableSet getWdMethodChecks(KeYJavaType kjt) {
+ assert kjt != null;
+ ImmutableSet result = DefaultImmutableSet.nil();
+ for (MethodWellDefinedness ch : getAllWdMethodChecks()) {
+ if (ch.getKJT().equals(kjt)) {
+ result = result.add(ch);
+ }
+ }
+ return result;
+ }
+
+ /**
+ * Returns all registered (atomic) well-definedness method checks for the passed target and kjt.
+ */
+ private ImmutableSet getWdMethodChecks(KeYJavaType kjt,
+ IObserverFunction target) {
+ assert kjt != null;
+ assert target != null;
+ ImmutableSet result = DefaultImmutableSet.nil();
+ for (MethodWellDefinedness ch : getAllWdMethodChecks()) {
+ if (ch.getKJT().equals(kjt) && ch.getTarget().equals(target)) {
+ result = result.add(ch);
+ }
+ }
+ return result;
+ }
+
+ /**
+ * Returns all registered (atomic) well-definedness class checks for the passed kjt.
+ */
+ private ImmutableSet getWdClassChecks(KeYJavaType kjt) {
+ ImmutableSet checks = getWdChecks(kjt);
+ ImmutableSet invs = DefaultImmutableSet.nil();
+ for (WellDefinednessCheck check : checks) {
+ if (check instanceof ClassWellDefinedness) {
+ invs = invs.add((ClassWellDefinedness) check);
+ }
+ }
+ return invs;
+ }
+
+ /**
+ * Registers a well-definedness check for a jml statement. It does not take care of its
+ * visibility in the proof management dialog.
+ *
+ * @param swd The well-definedness check
+ */
+ public void addWdStatement(StatementWellDefinedness swd) {
+ registerWdCheck(swd);
+ }
+
+ /**
+ * Returns all registered well-definedness checks.
+ */
+ public ImmutableSet getAllWdChecks() {
+ ImmutableSet result = DefaultImmutableSet.nil();
+ for (ImmutableSet s : wdChecks.values()) {
+ result = result.union(s);
+ }
+ return result;
+ }
+
+ /**
+ * Removes the contract from the repository, but keeps its target.
+ */
+ @Override
+ protected void unregisterContract(Contract contract) {
+ super.unregisterContract(contract);
+
+ final KeYJavaType kjt = contract.getKJT();
+
+ if (contract instanceof FunctionalOperationContract) {
+ if (!getWdChecks(contract.getKJT(), contract.getTarget()).isEmpty()) {
+ ImmutableSet wdcs =
+ getWdChecks(contract.getKJT(), contract.getTarget());
+ for (WellDefinednessCheck wdc : wdcs) {
+ if (wdc instanceof MethodWellDefinedness
+ && ((MethodWellDefinedness) wdc).getMethodContract().equals(contract)) {
+ unregisterWdCheck(wdc);
+ }
+ }
+ }
+ }
+
+ if (contract instanceof WellDefinednessCheck) {
+ unregisterWdCheck((WellDefinednessCheck) contract);
+ }
+
+ }
+
+ @Override
+ public void map(UnaryOperator op, Services services) {
+ super.map(op, services);
+ mapValueSets(wdChecks, op, services);
+ }
+
+
+ @Override
+ public ImmutableSet getAllContracts() {
+ var result = super.getAllContracts();
+ return WellDefinednessCheck.isOn(services) ? result : removeWdChecks(result);
+ }
+
+ @Override
+ public ImmutableSet getContracts(KeYJavaType kjt, IObserverFunction target) {
+ var result = super.getContracts(kjt, target);
+ if (WellDefinednessCheck.isOn(services))
+ return result;
+ else
+ return removeWdChecks(result);
+ }
+
+
+ /**
+ * Represent terms belong to model fields, so the well-definedness check considers both of them
+ * together.
+ *
+ * @param kjt The relevant KeYJavaType
+ */
+ @Override
+ public void processJavaType(KeYJavaType kjt) {
+ ImmutableSet axs = axioms.get(kjt);
+ if (axs == null) {
+ return;
+ }
+ ImmutableSet reps = DefaultImmutableSet.nil();
+ for (ClassAxiom ax : axs) {
+ if (ax instanceof RepresentsAxiom) {
+ reps = reps.add((RepresentsAxiom) ax);
+ }
+ }
+ final ProgramVariable heap = services.getTypeConverter().getHeapLDT().getHeap();
+ for (RepresentsAxiom rep : reps) {
+ boolean dep = false;
+ for (MethodWellDefinedness ch : getWdMethodChecks(kjt)) {
+ if (ch.modelField() && ch.getTarget().equals(rep.getTarget())) {
+ dep = true;
+ unregisterContract(ch);
+ JTerm represents = rep.getAxiom(heap, ch.getOrigVars().self, services);
+ WellDefinednessCheck newCh = ch.addRepresents(represents);
+ registerContract(newCh);
+ }
+ }
+ if (!dep) {
+ MethodWellDefinedness mwd = new MethodWellDefinedness(rep, services);
+ registerContract(mwd);
+ }
+ }
+ }
+
+ @Override
+ public void addClassInvariant(ClassInvariant inv) {
+ super.addClassInvariant(inv);
+
+ final KeYJavaType kjt = inv.getKJT();
+ final IObserverFunction target = inv.isStatic() ? services.getJavaInfo().getStaticInv(kjt)
+ : services.getJavaInfo().getInv();
+
+ final ImmutableSet cwds = getWdClassChecks(kjt);
+ if (cwds.isEmpty()) {
+ registerContract(new ClassWellDefinedness(inv, target, null, null, services));
+ } else {
+ assert cwds.size() == 1;
+ ClassWellDefinedness cwd = cwds.iterator().next();
+ unregisterContract(cwd);
+ cwd = cwd.combine(new ClassWellDefinedness(inv, cwd.getTarget(), null, null, services),
+ services);
+ registerContract(cwd);
+ }
+
+ // inherit non-private, non-static invariants
+ if (!inv.isStatic() && VisibilityModifier.allowsInheritance(inv.getVisibility())) {
+ final ImmutableList subs = services.getJavaInfo().getAllSubtypes(kjt);
+ for (KeYJavaType sub : subs) {
+ ClassInvariant subInv = inv.setKJT(sub);
+ final IObserverFunction subTarget =
+ subInv.isStatic() ? services.getJavaInfo().getStaticInv(sub)
+ : services.getJavaInfo().getInv();
+ final ImmutableSet subCwds = getWdClassChecks(sub);
+ if (subCwds.isEmpty()) {
+ registerContract(
+ new ClassWellDefinedness(subInv, subTarget, null, null, services));
+ } else {
+ for (ClassWellDefinedness cwd : subCwds) {
+ unregisterContract(cwd);
+ cwd.addInv(subInv.getInv(cwd.getOrigVars().self, services));
+ registerContract(cwd);
+ }
+ }
+ }
+ }
+ }
+
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/StatementWellDefinedness.java
similarity index 97%
rename from key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java
rename to key.core.wd/src/main/java/de/uka/ilkd/key/wd/StatementWellDefinedness.java
index 1ed6a8e0e21..590e3bbcabc 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/StatementWellDefinedness.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.speclang;
+package de.uka.ilkd.key.wd;
import java.util.LinkedHashMap;
import java.util.Map;
@@ -12,7 +12,9 @@
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.TermServices;
import de.uka.ilkd.key.logic.op.*;
-import de.uka.ilkd.key.proof.init.WellDefinednessPO.Variables;
+import de.uka.ilkd.key.speclang.ContractFactory;
+import de.uka.ilkd.key.speclang.SpecificationElement;
+import de.uka.ilkd.key.wd.po.WellDefinednessPO.Variables;
import org.key_project.logic.op.Function;
import org.key_project.prover.sequent.SequentFormula;
diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdBlockContractInternalRule.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdBlockContractInternalRule.java
new file mode 100644
index 00000000000..4fce32f8a88
--- /dev/null
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdBlockContractInternalRule.java
@@ -0,0 +1,49 @@
+/* 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.wd;
+
+import java.util.List;
+import java.util.Map;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.logic.op.LocationVariable;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.rule.BlockContractInternalRule;
+import de.uka.ilkd.key.speclang.BlockContract;
+
+import org.key_project.logic.op.Function;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSet;
+
+import static de.uka.ilkd.key.rule.AuxiliaryContractBuilders.GoalsConfigurator;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (7/27/25)
+ */
+public class WdBlockContractInternalRule extends BlockContractInternalRule {
+ public static final WdBlockContractInternalRule INSTANCE = new WdBlockContractInternalRule();
+
+ @Override
+ protected ImmutableList splitIntoGoals(Goal goal, BlockContract contract,
+ List heaps,
+ ImmutableSet localInVariables,
+ Map anonymisationHeaps,
+ JTerm contextUpdate, JTerm remembranceUpdate,
+ ImmutableSet localOutVariables,
+ GoalsConfigurator configurator, Services services) {
+ LocationVariable heap = heaps.getFirst();
+ var result = goal.split(4);
+ JTerm localAnonUpdate = createLocalAnonUpdate(localOutVariables, services);
+ JTerm wdUpdate = services.getTermBuilder().parallel(contextUpdate, remembranceUpdate);
+ WdFunctionalBlockContractPO.setUpWdGoal(
+ result.get(3), contract, wdUpdate,
+ localAnonUpdate, heap, anonymisationHeaps.get(heap), localInVariables,
+ configurator.services,
+ configurator.variables,
+ configurator.occurrence);
+ return result;
+ }
+}
diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdFunctionalBlockContractPO.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdFunctionalBlockContractPO.java
new file mode 100644
index 00000000000..a70ca14216e
--- /dev/null
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdFunctionalBlockContractPO.java
@@ -0,0 +1,132 @@
+/* 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.wd;
+
+import java.util.List;
+import java.util.Map;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.logic.TermBuilder;
+import de.uka.ilkd.key.logic.op.LocationVariable;
+import de.uka.ilkd.key.logic.op.ProgramVariable;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.init.FunctionalBlockContractPO;
+import de.uka.ilkd.key.proof.init.InitConfig;
+import de.uka.ilkd.key.rule.AuxiliaryContractBuilders;
+import de.uka.ilkd.key.speclang.AuxiliaryContract;
+import de.uka.ilkd.key.speclang.BlockContract;
+import de.uka.ilkd.key.speclang.FunctionalBlockContract;
+import de.uka.ilkd.key.wd.macro.WellDefinednessMacro;
+
+import org.key_project.logic.op.Function;
+import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.prover.sequent.SequentFormula;
+import org.key_project.util.collection.ImmutableSet;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (8/3/25)
+ */
+public class WdFunctionalBlockContractPO extends FunctionalBlockContractPO {
+ /**
+ * @param initConfig the initial proof configuration.
+ * @param contract the contract from which this PO is generated.
+ */
+ public WdFunctionalBlockContractPO(InitConfig initConfig, FunctionalBlockContract contract) {
+ super(initConfig, contract);
+ }
+
+ /**
+ * @param validity the validity formula.
+ * @param updates the updates.
+ * @param heaps the heaps.
+ * @param anonOutHeaps the heaps used in the anonOut update.
+ * @param localInVariables the free local variables in the block.
+ * @param localOutVariables the free local variables modifiable by the block.
+ * @param bc the contract being applied.
+ * @param configurator a goal configurator
+ * @param services services.
+ * @param tb a term builder.
+ * @return the conjunction of the well-definedness formula and the validity formula.
+ */
+ protected JTerm addWdToValidityTerm(JTerm validity, final JTerm[] updates,
+ final List heaps, Map anonOutHeaps,
+ final ImmutableSet localInVariables,
+ final ImmutableSet localOutVariables, final BlockContract bc,
+ final AuxiliaryContractBuilders.GoalsConfigurator configurator,
+ final Services services, final TermBuilder tb) {
+ if (WellDefinednessCheck.isOn(services)) {
+ final JTerm wdUpdate = services.getTermBuilder().parallel(updates[1], updates[2]);
+
+ JTerm localAnonUpdate = createLocalAnonUpdate(localOutVariables, services, tb);
+
+ if (localAnonUpdate == null) {
+ localAnonUpdate = tb.skip();
+ }
+
+ JTerm wellDefinedness = setUpWdGoal(null, bc, wdUpdate, localAnonUpdate,
+ heaps.getFirst(), anonOutHeaps.get(heaps.getFirst()), localInVariables,
+ services, null, null);
+
+ validity = tb.and(wellDefinedness, validity);
+ }
+ return validity;
+ }
+
+ @Override
+ protected JTerm setUpValidityTerm(List heaps,
+ Map anonHeaps, Map anonOutHeaps,
+ ImmutableSet localInVariables,
+ ImmutableSet localOutVariables, ProgramVariable exceptionParameter,
+ JTerm[] assumptions, JTerm[] postconditions, JTerm[] updates, BlockContract bc,
+ AuxiliaryContractBuilders.ConditionsAndClausesBuilder conditionsAndClausesBuilder,
+ AuxiliaryContractBuilders.GoalsConfigurator configurator, Services services,
+ TermBuilder tb) {
+ var validity = super.setUpValidityTerm(heaps, anonHeaps, anonOutHeaps, localInVariables,
+ localOutVariables, exceptionParameter, assumptions, postconditions, updates, bc,
+ conditionsAndClausesBuilder, configurator, services, tb);
+ return addWdToValidityTerm(validity, updates, heaps, anonOutHeaps, localInVariables,
+ localOutVariables, bc, configurator, services, tb);
+ }
+
+ /**
+ * @param goal If this is not {@code null}, the returned formula is added to this goal.
+ * @param contract the contract being applied.
+ * @param update the update.
+ * @param anonUpdate the anonymization update.
+ * @param heap the heap.
+ * @param anonHeap the anonymization heap.
+ * @param localIns all free local variables in the block.
+ * @param variables
+ * @param occurrence
+ * @return the well-definedness formula.
+ */
+ public static JTerm setUpWdGoal(final @Nullable Goal goal, final BlockContract contract,
+ final JTerm update,
+ final JTerm anonUpdate, final LocationVariable heap, final Function anonHeap,
+ final ImmutableSet localIns,
+ Services services,
+ AuxiliaryContract.Variables variables, PosInOccurrence occurrence) {
+ // FIXME: Handling of \old-references needs to be investigated,
+ // however only completeness is lost, soundness is guaranteed
+ final BlockWellDefinedness bwd =
+ new BlockWellDefinedness(contract, variables, localIns, services);
+ ((SpecificationRepositoryWD) services.getSpecificationRepository()).addWdStatement(bwd);
+ final LocationVariable heapAtPre = variables.remembranceHeaps.get(heap);
+ final JTerm anon = anonHeap != null ? services.getTermBuilder().func(anonHeap) : null;
+ final SequentFormula wdBlock = bwd.generateSequent(
+ variables.self, variables.exception,
+ variables.result, heap, heapAtPre, anon, localIns, update, anonUpdate, services);
+
+ if (goal != null) {
+ goal.setBranchLabel(WellDefinednessMacro.WD_BRANCH);
+ goal.changeFormula(wdBlock, occurrence);
+ }
+
+ return (JTerm) wdBlock.formula();
+ }
+}
diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java
new file mode 100644
index 00000000000..a8cc056e4be
--- /dev/null
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java
@@ -0,0 +1,102 @@
+/* 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.wd;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.init.InitConfig;
+import de.uka.ilkd.key.proof.init.JavaProfile;
+import de.uka.ilkd.key.proof.init.RuleCollection;
+import de.uka.ilkd.key.proof.io.RuleSource;
+import de.uka.ilkd.key.proof.io.RuleSourceFactory;
+import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+import de.uka.ilkd.key.rule.*;
+import de.uka.ilkd.key.util.KeYResourceManager;
+import org.key_project.logic.Name;
+import org.key_project.util.collection.ImmutableList;
+
+import java.net.URL;
+import java.util.Objects;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (7/27/25)
+ */
+public class WdProfile extends JavaProfile {
+ public static final String PROFILE_ID = "java-wd";
+ public static final String DISPLAY_NAME = "Java Profile + Well-Definedness Checks";
+
+ public static final WdProfile INSTANCE = new WdProfile();
+
+ private final RuleCollection wdStandardRules;
+
+ public WdProfile() {
+ super();
+
+ var defRules = super.getStandardRules();
+
+ final URL wdDotKey = KeYResourceManager.getManager().getResourceFile(Proof.class, "rules/wd.key");
+
+ RuleSource tacletBaseWd = RuleSourceFactory.initRuleFile(
+ Objects.requireNonNull(wdDotKey, "Could not find rule file 'rules/wd.key' in classpath"));
+
+ wdStandardRules = new RuleCollection(defRules.getTacletBase()
+ .append(tacletBaseWd),
+ defRules.standardBuiltInRules());
+ }
+
+ @Override
+ public String ident() {
+ return PROFILE_ID;
+ }
+
+ @Override
+ public String displayName() {
+ return DISPLAY_NAME;
+ }
+
+ @Override
+ public String description() {
+ return "A profile for the verification of Java programs with incl. " +
+ "well-definedness checks for JML specification. **Stability unknown**";
+ }
+
+ @Override
+ public SpecificationRepository createSpecificationRepository(Services services) {
+ return new SpecificationRepositoryWD(services);
+ }
+
+ @Override
+ protected ImmutableList initBuiltInRules() {
+ var javaRules = super.initBuiltInRules();
+ var rules = javaRules.map(it -> {
+ if (it instanceof BlockContractInternalRule) {
+ return WdBlockContractInternalRule.INSTANCE;
+ } else if (it instanceof WhileInvariantRule) {
+ return WdWhileInvariantRule.INSTANCE;
+ } else
+ return it;
+ })
+ .filter(it -> it != BlockContractExternalRule.INSTANCE)
+ .filter(it -> !(it instanceof LoopContractExternalRule))
+ .filter(it -> !(it instanceof LoopScopeInvariantRule));
+ return rules;
+ }
+
+ @Override
+ public boolean withPermissions() {
+ return false;
+ }
+
+ @Override
+ public RuleCollection getStandardRules() {
+ return wdStandardRules;
+ }
+
+ @Override
+ public void prepareInitConfig(InitConfig baseConfig) {
+ var wdChoice = baseConfig.choiceNS().lookup(new Name("wdChecks:on"));
+ baseConfig.activateChoice(wdChoice);
+ }
+}
diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfileResolver.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfileResolver.java
new file mode 100644
index 00000000000..06a7056fdf2
--- /dev/null
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfileResolver.java
@@ -0,0 +1,23 @@
+/* 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.wd;
+
+import de.uka.ilkd.key.proof.init.DefaultProfileResolver;
+import de.uka.ilkd.key.proof.init.Profile;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (8/3/25)
+ */
+public class WdProfileResolver implements DefaultProfileResolver {
+ @Override
+ public String getProfileName() {
+ return WdProfile.PROFILE_ID;
+ }
+
+ @Override
+ public Profile getDefaultProfile() {
+ return WdProfile.INSTANCE;
+ }
+}
diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java
new file mode 100644
index 00000000000..6ac0523eccc
--- /dev/null
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java
@@ -0,0 +1,74 @@
+/* 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.wd;
+
+import de.uka.ilkd.key.logic.op.LocationVariable;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.rule.LoopInvariantBuiltInRuleApp;
+import de.uka.ilkd.key.rule.WhileInvariantRule;
+import de.uka.ilkd.key.wd.macro.WellDefinednessMacro;
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+import org.key_project.logic.Name;
+import org.key_project.prover.rules.RuleAbortException;
+import org.key_project.prover.rules.RuleApp;
+import org.key_project.prover.sequent.SequentFormula;
+import org.key_project.util.collection.ImmutableList;
+
+
+@NullMarked
+public class WdWhileInvariantRule extends WhileInvariantRule {
+ private static final Name NAME = new Name("WD Loop Invariant");
+ public static final int IDX_GOAL_WD = 1 + WhileInvariantRuleApplier.IDX_GOAL_INIT;
+ public static final WdWhileInvariantRule INSTANCE = new WdWhileInvariantRule();
+
+ @Override
+ public @NonNull ImmutableList apply(Goal goal, RuleApp ruleApp)
+ throws RuleAbortException {
+ return new WdWhileInvariantRuleApplier(goal, (LoopInvariantBuiltInRuleApp>) ruleApp)
+ .apply();
+ }
+
+ @Override
+ public Name name() {
+ return NAME;
+ }
+
+ @Override
+ public @Nullable String getOrigin() {
+ return super.getOrigin();
+ }
+
+ protected static class WdWhileInvariantRuleApplier extends WhileInvariantRuleApplier {
+ public WdWhileInvariantRuleApplier(Goal goal, LoopInvariantBuiltInRuleApp> ruleApp) {
+ super(goal, ruleApp);
+ }
+
+ @Override
+ public @NonNull ImmutableList apply() {
+ final ImmutableList result = goal.split(4);
+ super.prepareGoals(result);
+ setupWdGoal(result.get(IDX_GOAL_WD));
+ return result;
+
+ }
+
+ private void setupWdGoal(Goal goal) {
+ goal.setBranchLabel(WellDefinednessMacro.WD_BRANCH);
+ final LoopWellDefinedness lwd = new LoopWellDefinedness(inst.inv(), localIns, services);
+ final LocationVariable self;
+ if (inst.selfTerm().op() instanceof LocationVariable lv) {
+ self = lv;
+ } else {
+ self = null;
+ }
+ ((SpecificationRepositoryWD) services.getSpecificationRepository()).addWdStatement(lwd);
+ LocationVariable heap = heapContext.getFirst();
+ final SequentFormula wdInv = lwd.generateSequent(self, heap, anonHeap, localIns,
+ inst.u(), localAnonUpdate, services);
+ goal.changeFormula(wdInv, ruleApp.posInOccurrence());
+ }
+ }
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WellDefinednessCheck.java
similarity index 98%
rename from key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
rename to key.core.wd/src/main/java/de/uka/ilkd/key/wd/WellDefinednessCheck.java
index b910b2988b9..048da11526f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WellDefinednessCheck.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.speclang;
+package de.uka.ilkd.key.wd;
import java.util.Iterator;
import java.util.LinkedHashMap;
@@ -20,14 +20,15 @@
import de.uka.ilkd.key.proof.OpReplacer;
import de.uka.ilkd.key.proof.init.ContractPO;
import de.uka.ilkd.key.proof.init.InitConfig;
+import de.uka.ilkd.key.proof.init.Profile;
import de.uka.ilkd.key.proof.init.ProofOblInput;
-import de.uka.ilkd.key.proof.init.WellDefinednessPO;
-import de.uka.ilkd.key.proof.init.WellDefinednessPO.Variables;
import de.uka.ilkd.key.rule.RewriteTaclet;
import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletBuilder;
-import de.uka.ilkd.key.settings.ProofSettings;
+import de.uka.ilkd.key.speclang.Contract;
import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor;
import de.uka.ilkd.key.util.MiscTools;
+import de.uka.ilkd.key.wd.po.WellDefinednessPO;
+import de.uka.ilkd.key.wd.po.WellDefinednessPO.Variables;
import org.key_project.logic.Name;
import org.key_project.logic.op.Function;
@@ -53,6 +54,7 @@ public abstract class WellDefinednessCheck implements Contract {
public static final String OP_TACLET = "wd_Operation";
public static final String OP_EXC_TACLET = "wd_Exc_Operation";
+
enum Type {
CLASS_INVARIANT, OPERATION_CONTRACT, LOOP_INVARIANT, BLOCK_CONTRACT
}
@@ -944,20 +946,27 @@ public WellDefinednessCheck combine(WellDefinednessCheck wdc, TermServices servi
*
* @return true if on and false if off
*/
- public static boolean isOn() {
- final String setting =
- ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices().get(OPTION);
- if (setting == null) {
- return false;
- }
- if (setting.equals(OPTION + ":on")) {
- return true;
- } else if (setting.equals(OPTION + ":off")) {
- return false;
- } else {
- throw new RuntimeException(
- "The setting for the wdProofs-option is not valid: " + setting);
- }
+ public static boolean isOn(Profile profile) {
+ return profile instanceof WdProfile;
+ }
+
+ public static boolean isOn(Services services) {
+ return isOn(services.getProfile());
+ /*
+ * final String setting =
+ * ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices().get(OPTION);
+ * if (setting == null) {
+ * return false;
+ * }
+ * if (setting.equals(OPTION + ":on")) {
+ * return true;
+ * } else if (setting.equals(OPTION + ":off")) {
+ * return false;
+ * } else {
+ * throw new RuntimeException(
+ * "The setting for the wdProofs-option is not valid: " + setting);
+ * }
+ */
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/WellDefinednessMacro.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/macro/WellDefinednessMacro.java
similarity index 94%
rename from key.core/src/main/java/de/uka/ilkd/key/macros/WellDefinednessMacro.java
rename to key.core.wd/src/main/java/de/uka/ilkd/key/wd/macro/WellDefinednessMacro.java
index bcaaacb0e5f..21bdf9cf3d8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/macros/WellDefinednessMacro.java
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/macro/WellDefinednessMacro.java
@@ -1,17 +1,18 @@
/* 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.macros;
+package de.uka.ilkd.key.wd.macro;
+import de.uka.ilkd.key.macros.StrategyProofMacro;
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.init.ContractPO;
import de.uka.ilkd.key.proof.init.FunctionalOperationContractPO;
-import de.uka.ilkd.key.proof.init.WellDefinednessPO;
-import de.uka.ilkd.key.speclang.WellDefinednessCheck;
import de.uka.ilkd.key.strategy.RuleAppCostCollector;
import de.uka.ilkd.key.strategy.Strategy;
+import de.uka.ilkd.key.wd.*;
+import de.uka.ilkd.key.wd.po.*;
import org.key_project.logic.Name;
import org.key_project.prover.proof.ProofGoal;
@@ -64,7 +65,8 @@ public String getDescription() {
@Override
public boolean canApplyTo(Proof proof, ImmutableList goals,
PosInOccurrence posInOcc) {
- if (proof == null || proof.isDisposed() || !WellDefinednessCheck.isOn()) {
+ if (proof == null || proof.isDisposed()
+ || !WellDefinednessCheck.isOn(proof.getServices())) {
return false;
}
final ContractPO po = proof.getServices().getSpecificationRepository().getPOForProof(proof);
diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WDTacletGenerator.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WDTacletGenerator.java
new file mode 100644
index 00000000000..84d41d6ff64
--- /dev/null
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WDTacletGenerator.java
@@ -0,0 +1,75 @@
+/* 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.wd.po;
+
+import de.uka.ilkd.key.proof.init.AbstractPO;
+import de.uka.ilkd.key.proof.init.InitConfig;
+import de.uka.ilkd.key.proof.init.TacletPOGenerator;
+import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+import de.uka.ilkd.key.rule.RewriteTaclet;
+import de.uka.ilkd.key.wd.ClassWellDefinedness;
+import de.uka.ilkd.key.wd.MethodWellDefinedness;
+import de.uka.ilkd.key.wd.SpecificationRepositoryWD;
+import de.uka.ilkd.key.wd.WellDefinednessCheck;
+
+import org.key_project.util.collection.DefaultImmutableSet;
+import org.key_project.util.collection.ImmutableSet;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (1/1/26)
+ */
+public class WDTacletGenerator implements TacletPOGenerator {
+ /**
+ * Generate well-definedness taclets to resolve formulas as WD(pv.{@literal }) or
+ * WD(pv.m(...)).
+ *
+ * @param proofConfig the proof configuration
+ */
+ @Override
+ public void generate(AbstractPO abstractPO, InitConfig proofConfig,
+ SpecificationRepository specRepos) {
+ if (!WellDefinednessCheck.isOn(proofConfig.getProfile())) {
+ return;
+ }
+ ImmutableSet res = DefaultImmutableSet.nil();
+ ImmutableSet names = DefaultImmutableSet.nil();
+
+ var repo = (SpecificationRepositoryWD) specRepos;
+ for (WellDefinednessCheck ch : repo.getAllWdChecks()) {
+ if (ch instanceof MethodWellDefinedness mwd) {
+ // WD(callee.m(...))
+ RewriteTaclet mwdTaclet = mwd.createOperationTaclet(proofConfig.getServices());
+ String tName = mwdTaclet.name().toString();
+ final String prefix;
+ if (tName.startsWith(WellDefinednessCheck.OP_TACLET)) {
+ prefix = WellDefinednessCheck.OP_TACLET;
+ } else if (tName.startsWith(WellDefinednessCheck.OP_EXC_TACLET)) {
+ prefix = WellDefinednessCheck.OP_EXC_TACLET;
+ } else {
+ prefix = "";
+ }
+ tName = tName.replace(prefix, "");
+ if (names.contains(tName)) {
+ for (RewriteTaclet t : res) {
+ if (t.find().toString().equals(mwdTaclet.find().toString())) {
+ res = res.remove(t);
+ names = names.remove(tName);
+ mwdTaclet = mwd.combineTaclets(t, mwdTaclet, proofConfig.getServices());
+ }
+ }
+ }
+ res = res.add(mwdTaclet);
+ names = names.add(tName);
+ }
+ }
+
+ // WD(a.)
+ res = res.union(ClassWellDefinedness.createInvTaclet(proofConfig.getServices()));
+ for (RewriteTaclet t : res) {
+ abstractPO.register(t, proofConfig);
+ }
+ }
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WellDefinednessPO.java
similarity index 96%
rename from key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
rename to key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WellDefinednessPO.java
index 37f9275ec6a..b74fc06d189 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WellDefinednessPO.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.proof.init;
+package de.uka.ilkd.key.wd.po;
import java.util.LinkedHashMap;
import java.util.Map;
@@ -12,13 +12,17 @@
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.label.ParameterlessTermLabel;
import de.uka.ilkd.key.logic.op.*;
+import de.uka.ilkd.key.proof.init.AbstractPO;
+import de.uka.ilkd.key.proof.init.ContractPO;
+import de.uka.ilkd.key.proof.init.InitConfig;
+import de.uka.ilkd.key.proof.init.ProofOblInput;
import de.uka.ilkd.key.settings.Configuration;
import de.uka.ilkd.key.speclang.ClassAxiom;
-import de.uka.ilkd.key.speclang.ClassWellDefinedness;
import de.uka.ilkd.key.speclang.Contract.OriginalVariables;
-import de.uka.ilkd.key.speclang.WellDefinednessCheck;
-import de.uka.ilkd.key.speclang.WellDefinednessCheck.POTerms;
-import de.uka.ilkd.key.speclang.WellDefinednessCheck.TermAndFunc;
+import de.uka.ilkd.key.wd.ClassWellDefinedness;
+import de.uka.ilkd.key.wd.WellDefinednessCheck;
+import de.uka.ilkd.key.wd.WellDefinednessCheck.POTerms;
+import de.uka.ilkd.key.wd.WellDefinednessCheck.TermAndFunc;
import org.key_project.logic.Name;
import org.key_project.logic.op.Function;
@@ -256,7 +260,7 @@ public void readProblem() {
// add axioms
collectClassAxioms(getKJT(), proofConfig);
- generateWdTaclets(proofConfig);
+ generateDynamicTaclets(proofConfig);
}
private Services postInit() {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPOLoader.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WellDefinednessPOLoader.java
similarity index 72%
rename from key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPOLoader.java
rename to key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WellDefinednessPOLoader.java
index 08aca51e25b..02b526c2fa8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPOLoader.java
+++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/po/WellDefinednessPOLoader.java
@@ -1,13 +1,18 @@
/* 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.init;
+package de.uka.ilkd.key.wd.po;
+import de.uka.ilkd.key.proof.init.IPersistablePO;
+import de.uka.ilkd.key.proof.init.InitConfig;
+import de.uka.ilkd.key.proof.init.ProofOblInput;
import de.uka.ilkd.key.proof.init.loader.ProofObligationLoader;
import de.uka.ilkd.key.settings.Configuration;
import de.uka.ilkd.key.speclang.Contract;
import org.jspecify.annotations.NullMarked;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
/**
* Loader for proof obligation arises from well definedness.
@@ -17,6 +22,8 @@
*/
@NullMarked
public class WellDefinednessPOLoader implements ProofObligationLoader {
+ private static final Logger LOGGER = LoggerFactory.getLogger(WellDefinednessPOLoader.class);
+
/**
* Instantiates a new proof obligation with the given settings.
*
@@ -31,6 +38,13 @@ public IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig,
final Contract contract =
initConfig.getServices().getSpecificationRepository().getContractByName(contractName);
if (contract == null) {
+ LOGGER.error("Contract {} not found.", contractName);
+ var c = initConfig.getServices().getSpecificationRepository();
+ LOGGER.info("Available contracts: ");
+ for (var contr : c.getAllContracts()) {
+ LOGGER.info("Name:{}, Display: {}", contr.getName(), contr.getDisplayName());
+ }
+
throw new RuntimeException("Contract not found: " + contractName);
} else {
final ProofOblInput po = contract.createProofObl(initConfig);
diff --git a/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro b/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro
new file mode 100644
index 00000000000..edb3fab51a2
--- /dev/null
+++ b/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.macros.ProofMacro
@@ -0,0 +1 @@
+de.uka.ilkd.key.wd.macro.WellDefinednessMacro
diff --git a/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver b/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver
new file mode 100644
index 00000000000..eb3cf6569ed
--- /dev/null
+++ b/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver
@@ -0,0 +1 @@
+de.uka.ilkd.key.wd.WdProfileResolver
diff --git a/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.TacletPOGenerator b/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.TacletPOGenerator
new file mode 100644
index 00000000000..823096a0aef
--- /dev/null
+++ b/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.TacletPOGenerator
@@ -0,0 +1 @@
+de.uka.ilkd.key.wd.po.WDTacletGenerator
\ No newline at end of file
diff --git a/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.loader.ProofObligationLoader b/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.loader.ProofObligationLoader
new file mode 100644
index 00000000000..d89ff51bb4c
--- /dev/null
+++ b/key.core.wd/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.loader.ProofObligationLoader
@@ -0,0 +1 @@
+de.uka.ilkd.key.wd.po.WellDefinednessPOLoader
\ No newline at end of file
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wd.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wd.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wd.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wd.key
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdFormulaRules.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdFormulaRules.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdFormulaRules.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdFormulaRules.key
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdGeneralRules.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdGeneralRules.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdGeneralRules.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdGeneralRules.key
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeader.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeader.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeader.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeader.key
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeapRules.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeapRules.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeapRules.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeapRules.key
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdLocSetRules.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdLocSetRules.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdLocSetRules.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdLocSetRules.key
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdNumericalRules.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdNumericalRules.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdNumericalRules.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdNumericalRules.key
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdReachRules.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdReachRules.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdReachRules.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdReachRules.key
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdRegExRules.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdRegExRules.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdRegExRules.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdRegExRules.key
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdSeqRules.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdSeqRules.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdSeqRules.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdSeqRules.key
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdStringRules.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdStringRules.key
similarity index 100%
rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdStringRules.key
rename to key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdStringRules.key
diff --git a/key.core.wd/src/test/java/de/uka/ilkd/key/wd/GenerateUnitTests.java b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/GenerateUnitTests.java
new file mode 100644
index 00000000000..fa607a3ccce
--- /dev/null
+++ b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/GenerateUnitTests.java
@@ -0,0 +1,41 @@
+/* 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.wd;
+
+import java.io.IOException;
+import java.nio.file.Paths;
+import java.util.List;
+
+import de.uka.ilkd.key.proof.runallproofs.ProofCollections;
+
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import static de.uka.ilkd.key.proof.runallproofs.GenerateUnitTests.*;
+
+/**
+ * Generation of test cases (JUnit) for given proof collection files.
+ *
+ * This class is intended to be called from gradle. See the gradle task
+ * {@code generateRunAllProofs}.
+ *
+ * The considered proof collections files are configured statically in
+ * {@link ProofCollections}.
+ *
+ * @author Alexander Weigl
+ * @version 1 (6/14/20)
+ */
+public class GenerateUnitTests {
+ private static final Logger LOGGER = LoggerFactory.getLogger(GenerateUnitTests.class);
+
+ public static void main(String[] args) throws IOException {
+ var collections = List.of(WdProofCollection.automaticWd());
+ if (args.length != 1) {
+ System.err.println("Usage: ");
+ System.exit(1);
+ }
+ var outputFolder = Paths.get(args[0]);
+ run(outputFolder, collections);
+ }
+}
diff --git a/key.core.wd/src/test/java/de/uka/ilkd/key/wd/RunAllProofsWd.java b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/RunAllProofsWd.java
new file mode 100644
index 00000000000..a7198e2010c
--- /dev/null
+++ b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/RunAllProofsWd.java
@@ -0,0 +1,34 @@
+/* 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.wd;
+
+import java.io.IOException;
+import java.util.stream.Stream;
+
+import de.uka.ilkd.key.proof.runallproofs.RunAllProofsTest;
+import de.uka.ilkd.key.proof.runallproofs.proofcollection.StatisticsFile;
+
+import org.junit.jupiter.api.Assumptions;
+import org.junit.jupiter.api.DynamicTest;
+import org.junit.jupiter.api.Tag;
+import org.junit.jupiter.api.TestFactory;
+
+/**
+ * This test case captures all information flow run-all-proof scenarios.
+ *
+ * @author M. Ulbrich
+ */
+@Tag("slow")
+@Tag("owntest")
+@Tag("testRunAllProofs")
+public final class RunAllProofsWd {
+ @TestFactory
+ Stream data() throws IOException {
+ var proofCollection = WdProofCollection.automaticWd();
+ StatisticsFile statisticsFile = proofCollection.getSettings().getStatisticsFile();
+ statisticsFile.setUp();
+ Assumptions.assumeTrue(proofCollection != null);
+ return RunAllProofsTest.data(proofCollection);
+ }
+}
diff --git a/key.core.wd/src/test/java/de/uka/ilkd/key/wd/WdProofCollection.java b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/WdProofCollection.java
new file mode 100644
index 00000000000..3cb4b123224
--- /dev/null
+++ b/key.core.wd/src/test/java/de/uka/ilkd/key/wd/WdProofCollection.java
@@ -0,0 +1,201 @@
+/* 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.wd;
+
+import java.io.IOException;
+import java.util.Date;
+
+import de.uka.ilkd.key.proof.runallproofs.proofcollection.ForkMode;
+import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollection;
+import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollectionSettings;
+
+import static de.uka.ilkd.key.proof.runallproofs.ProofCollections.loadFromFile;
+import static org.assertj.core.api.Assertions.assertThat;
+
+public class WdProofCollection {
+ public static ProofCollection automaticWd() throws IOException {
+ var settings = new ProofCollectionSettings(new Date());
+ /*
+ * Defines a base directory.
+ * All paths in this file are treated relative to base directory (except path for base
+ * directory itself).
+ */
+ settings.setBaseDirectory("../key.ui/examples/");
+
+ /*
+ * Defines a statistics file.
+ * Path is relative to base directory.
+ */
+ settings.setStatisticsFile("build/reports/runallproofs/runStatistics.csv");
+
+ /*
+ * Fork mode setting, can be declared to create subprocesses while running tests declared in
+ * this file.
+ * Possible modes: noFork-all files are proven within a single process
+ * pervar g = c.group("- one subprocess is created for each group
+ * perFile-one subprocess is created for each file
+ */
+ settings.setForkMode(ForkMode.PERGROUP);
+
+ /*
+ * Enable or disable proof reloading.
+ * If enabled, closed proofs will be saved and reloaded after prover is finished.
+ */
+ settings.setReloadEnabled(true);
+
+ /*
+ * Temporary directory, which is used for inter process communication when using forked
+ * mode.
+ * The given path is relative to baseDirectory.
+ */
+ settings.setTempDir("build/runallproofs_wd_tmp");
+
+ /*
+ * If the fork mode is not set to noFork, the launched subprocesses are terminated as
+ * soon as the timeout specified here has elapsed. No timeout occurs if not specified.
+ *
+ * Timeout per subprocess in seconds
+ */
+ settings.setForkTimeout(2000);
+
+ /*
+ * If the fork mode is not set to noFork, the launched subprocesses
+ * get the specified amount of heap memory.
+ *
+ * Heap memory for subprocesses (like 500m or 2G)
+ */
+ // forkMemory = 1000m
+
+ /*
+ * To run the forked JVM in debug mode, set the TCP port to listen to here.
+ * You can prefix the port with "wait:" to make the JVM suspend till the
+ * process has connected.
+ *
+ * Examples: forkDebugPort = "8000"
+ * forkDebugPort = "wait:1234"
+ */
+ // forkDebugPort = "wait:1234"
+
+ /*
+ * By default, runAllProofs does not print a lot of information.
+ * Set this to true to get more output.
+ */
+ settings.setVerboseOutput(true);
+ // verboseOutput = true
+
+ /*
+ * By default, runAllProofs runs all groups in this file.
+ * By naming a comma separated list of groups here, the
+ * test can be restricted to these groups (for debugging).
+ */
+ // runOnlyOn = group1, group2 (the space after each comma is mandatory)
+ // settings.setRunOnlyOn("performance, performancePOConstruction");
+
+ settings.setKeySettings(loadFromFile("automaticJAVADL.properties"));
+
+
+ // // Tests for information flow
+ var c = new ProofCollection(settings);
+
+ var g = c.group("wd_revarray");
+ g.notprovable("./firstTouch/05-ReverseArray/reverse2WD.key");
+ g.provable("./firstTouch/05-ReverseArray/reverse2WD_Y.key");
+ g.notprovable("./firstTouch/06-BinarySearch/searchWD.key");
+ // does not exists anymore
+ // g.notprovable("./firstTouch/07-Cell/CellClient_mWD.key");
+ // g.provable("./firstTouch/07-Cell/Cell_CellWD.key");
+ // g.provable("./firstTouch/07-Cell/Cell_getXWD.key");
+ // g.provable("./firstTouch/07-Cell/Cell_setXWD.key");
+
+ g = c.group("wd_java5");
+ g.provable("./firstTouch/08-Java5/For_infiniteLoopWD.key");
+ g.provable("./firstTouch/08-Java5/For_infiniteLoopWithWDLoop.key");
+ g.provable("./firstTouch/08-Java5/For_invariantWD.key");
+ g.provable("./firstTouch/08-Java5/For_sumWD.key");
+ g.notprovable("./firstTouch/08-Java5/For_sumWithWDLoop.key");
+
+ g = c.group("wd_quicktour");
+ g.provable("./firstTouch/09-Quicktour/CardException_getCauseWD.key");
+ g.provable("./firstTouch/09-Quicktour/CardException_getMessageWD.key");
+ g.provable("./firstTouch/09-Quicktour/CardException_initCauseWD.key");
+ g.provable("./firstTouch/09-Quicktour/LogFile_LogFileWD.key");
+ g.provable("./firstTouch/09-Quicktour/LogFile_LogFileWithWDLoop.key");
+ g.provable("./firstTouch/09-Quicktour/LogFile_addRecordWD.key");
+ g.provable("./firstTouch/09-Quicktour/LogFile_getMaximumRecordWD.key");
+ g.provable("./firstTouch/09-Quicktour/LogFile_getMaximumRecordWithWDLoop.key");
+ g.provable("./firstTouch/09-Quicktour/LogFile_invariantWD.key");
+ g.provable("./firstTouch/09-Quicktour/LogRecord_getBalanceWD.key");
+ g.provable("./firstTouch/09-Quicktour/LogRecord_getTransactionIdWD.key");
+ g.provable("./firstTouch/09-Quicktour/LogRecord_invariantWD.key");
+ g.provable("./firstTouch/09-Quicktour/LogRecord_setRecordWD.key");
+ g.provable("./firstTouch/09-Quicktour/PayCard_PayCardWD.key");
+ g.provable("./firstTouch/09-Quicktour/PayCard_PayCardintWD.key");
+ g.provable("./firstTouch/09-Quicktour/PayCard__chargeExcWD.key");
+ g.provable("./firstTouch/09-Quicktour/PayCard_chargeAndRecordWD.key");
+ g.provable("./firstTouch/09-Quicktour/PayCard_chargeWD.0.key");
+ g.provable("./firstTouch/09-Quicktour/PayCard_chargeWD.1.key");
+ g.provable("./firstTouch/09-Quicktour/PayCard_createJuniorCardWD.key");
+ g.provable("./firstTouch/09-Quicktour/PayCard_invariantWD.key");
+ g.provable("./firstTouch/09-Quicktour/PayCard_isValidWD.key");
+
+ g = c.group("wd_sita");
+ g.provable("./firstTouch/10-SITA/SITA3_commonEntryWD.key");
+ g.provable("./firstTouch/10-SITA/SITA3_commonEntryWithWDLoop.key");
+ g.provable("./firstTouch/10-SITA/SITA3_invariantWD.key");
+ g.provable("./firstTouch/10-SITA/SITA3_rearrangeWD.key");
+ g.provable("./firstTouch/10-SITA/SITA3_rearrangeWithWDLoop.key");
+ g.provable("./firstTouch/10-SITA/SITA3_swapWD.key");
+
+ g = c.group("wd_blockcontracts");
+ g.notprovable("./heap/block_contracts/GreatestCommonDivisor_ofWithWD.key");
+
+ g = c.group("wd_fm12_01_LRS");
+ g.notprovable("./heap/fm12_01_LRS/LCP_lcpWD.key");
+ g.notprovable("./heap/fm12_01_LRS/LRS_doLRSWD.key");
+ g.notprovable("./heap/fm12_01_LRS/SuffixArray_invariantWD.key");
+ g.notprovable("./heap/fm12_02_PrefixSum/PrefixSumRec_minWD.key");
+
+ g = c.group("wd_list");
+ g.notprovable("./heap/list_recursiveSpec/ListOperationsNonNull_getNextNNWD.key");
+ g.notprovable("./heap/list_seq/ArrayList_newArrayWD.key");
+ g.provable("./heap/list_seq/ArrayList_newArrayWD_Y.key");
+ g.notprovable("./heap/list_seq/SimplifiedLinkedList_getNextWD.key");
+ g.notprovable("./heap/list_seq/SimplifiedLinkedList_invariantWD.key");
+ g.notprovable("./heap/list_seq/TestLists_appendWD.key");
+
+ g = c.group("wd_otherheap");
+ g.notprovable("./heap/observer/ExampleSubject_valueWD.key");
+ g.notprovable("./heap/saddleback_search/Saddleback_searchWD.key");
+ g.provable("./heap/saddleback_search/Saddleback_searchWithWDLoop.key");
+ g.notprovable("./heap/vacid0_01_SparseArray/Harness_sparseArrayTestHarness1WD.key");
+
+ g = c.group("wd_vstte10_sam");
+ g.provable("./heap/vstte10_01_SumAndMax/SumAndMax_sumAndMaxWD.key");
+ g.provable("./heap/vstte10_01_SumAndMax/SumAndMax_sumAndMaxWithWDLoop.key");
+
+ g = c.group("wd_vstte10_ll");
+ g.provable("./heap/vstte10_03_LinkedList/Node_consWD.key");
+ g.provable("./heap/vstte10_03_LinkedList/Node_invWD.key");
+ g.provable("./heap/vstte10_03_LinkedList/Node_searchWD.key");
+
+
+ g = c.group("wd_vstte10_queens");
+ g.notprovable("./heap/vstte10_04_Queens/Queens_nQueensWD.key");
+ g.notprovable("./heap/vstte10_04_Queens/Queens_searchWD.key");
+ g.notprovable("./heap/vstte10_05_Queue/LinkedList_tailWD.key");
+
+ for (var testFile : g.getTestFiles()) {
+ try {
+ assertThat(testFile.getKeYFile())
+ .exists()
+ .content().contains("\\profile \"java-wd\";");
+ } catch (AssertionError e) {
+ System.err.println(testFile.getKeYFile());
+ throw e;
+ }
+ }
+
+ return c;
+ }
+}
diff --git a/key.core/build.gradle b/key.core/build.gradle
index a9eb7dcbc69..2645553ba50 100644
--- a/key.core/build.gradle
+++ b/key.core/build.gradle
@@ -129,15 +129,6 @@ tasks.register('testRunAllFunProofs', Test) {
}
}
-tasks.register('testRunAllInfProofs', Test) {
- description = 'Prove/reload all keyfiles tagged for regression testing'
- group = "verification"
- filter {
- includeTestsMatching "RunAllProofsInfFlow"
- }
-}
-
-
tasks.register('testProveSMTLemmas', Test) {
description = 'Prove (or load proofs for) lemmas used in the SMT translation'
group = "verification"
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..74e7e5c33b7 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
@@ -37,7 +37,7 @@
*
* @author Martin Hentschel
*/
-public class KeYEnvironment {
+public class KeYEnvironment implements AutoCloseable {
/**
* The {@link UserInterfaceControl} in which the {@link Proof} is loaded.
*/
@@ -354,4 +354,9 @@ public List getProofContracts() {
}
return proofContracts;
}
+
+ @Override
+ public void close() throws Exception {
+ dispose();
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowCompositePO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowCompositePO.java
deleted file mode 100644
index 80b66e4974d..00000000000
--- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowCompositePO.java
+++ /dev/null
@@ -1,15 +0,0 @@
-/* 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.informationflow.po;
-
-
-/**
- *
- * @author christoph
- */
-public interface InfFlowCompositePO extends InfFlowPO {
-
- AbstractInfFlowPO getChildPO();
-
-}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java
index 845fabb5d6f..3dd453a9246 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java
@@ -103,7 +103,7 @@ public Services(Profile profile) {
this.caches = new ServiceCaches();
this.termBuilder = new TermBuilder(new TermFactory(caches.getTermFactoryCache()), this);
this.termBuilderWithoutCache = new TermBuilder(new TermFactory(), this);
- this.specRepos = new SpecificationRepository(this);
+ this.specRepos = profile.createSpecificationRepository(this);
cee = new ConstantExpressionEvaluator(this);
typeconverter = new TypeConverter(this);
javainfo = new JavaInfo(
@@ -122,7 +122,7 @@ private Services(Profile profile, KeYCrossReferenceServiceConfiguration crsc,
this.caches = caches;
this.termBuilder = new TermBuilder(new TermFactory(caches.getTermFactoryCache()), this);
this.termBuilderWithoutCache = new TermBuilder(new TermFactory(), this);
- this.specRepos = new SpecificationRepository(this);
+ this.specRepos = profile.createSpecificationRepository(this);
cee = new ConstantExpressionEvaluator(this);
typeconverter = new TypeConverter(this);
javainfo = new JavaInfo(new KeYProgModelInfo(this, crsc, rec2key, typeconverter), this);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java
index 94fa2803998..5245820c84e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java
@@ -3,11 +3,9 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof;
-import java.util.ArrayList;
-import java.util.Collection;
-import java.util.LinkedList;
-import java.util.List;
+import java.util.*;
import java.util.concurrent.atomic.AtomicLong;
+import java.util.function.Consumer;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.NamespaceSet;
@@ -543,7 +541,7 @@ public void removeLastAppliedRuleApp() {
* @param n number of goals to create
* @return the list of new created goals.
*/
- public @NonNull ImmutableList split(int n) {
+ public @NonNull ImmutableList<@NonNull Goal> split(int n) {
ImmutableList goalList = ImmutableSLList.nil();
final Node parent = node; // has to be stored because the node
@@ -579,6 +577,20 @@ public void removeLastAppliedRuleApp() {
return goalList;
}
+ /// Creates new nodes as children of the referenced node and apply each given
+ /// non-null goal transformer to each proof.
+ ///
+ /// @return the list of new created goals, manipulated by funcs
+ public @NonNull ImmutableList split(List<@Nullable Consumer> funcs) {
+ final var nonNullFuncs = funcs.stream().filter(Objects::nonNull).toList();
+ var n = nonNullFuncs.size();
+ var goals = split(n);
+ for (int i = 0; i < n; i++) {
+ nonNullFuncs.get(i).accept(goals.get(i));
+ }
+ return goals;
+ }
+
public void setBranchLabel(String s) {
node.getNodeInfo().setBranchLabel(s);
}
@@ -699,7 +711,7 @@ public String toString() {
return lp.result();
}
- public T getStrategyInfo(Property property) {
+ public @Nullable T getStrategyInfo(Property property) {
return strategyInfos.get(property);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
index 06512119546..a6f5cab1498 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
@@ -5,6 +5,7 @@
import java.beans.PropertyChangeListener;
import java.io.File;
+import java.io.PrintWriter;
import java.nio.file.Path;
import java.util.*;
import java.util.function.Consumer;
@@ -12,7 +13,8 @@
import de.uka.ilkd.key.java.JavaInfo;
import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.*;
+import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.logic.NamespaceSet;
import de.uka.ilkd.key.pp.AbbrevMap;
import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit;
import de.uka.ilkd.key.proof.event.ProofDisposedEvent;
@@ -61,7 +63,7 @@ public class Proof implements ProofObject, Named {
/**
* The time when the {@link Proof} instance was created.
*/
- final long creationTime = System.currentTimeMillis();
+ private final long creationTime = System.currentTimeMillis();
/**
* name of the proof
@@ -124,7 +126,7 @@ public class Proof implements ProofObject, Named {
* when different users load and save a proof this vector fills up with Strings containing the
* usernames.
*/
- public List userLog;
+ public @Nullable List userLog;
/**
* when load and save a proof with different versions of key this vector fills up with Strings
@@ -1368,4 +1370,14 @@ public void copyCachedGoals(Proof referencedFrom,
}
}
}
+
+ /// Persist symbols (sorts, functions, ...) to the given `ps`.
+ /// There should be no need to write of [#header()].
+ public void printSymbols(PrintWriter ps) {
+ }
+
+ /// The time when the {@link Proof} instance was created.
+ public long getCreationTime() {
+ return creationTime;
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java
index b5cd2031913..d0fb54e4aa9 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java
@@ -8,8 +8,6 @@
import java.util.Iterator;
import java.util.List;
-import de.uka.ilkd.key.informationflow.proof.InfFlowProof;
-import de.uka.ilkd.key.informationflow.proof.SideProofStatistics;
import de.uka.ilkd.key.proof.reference.ClosedBy;
import de.uka.ilkd.key.rule.*;
import de.uka.ilkd.key.rule.OneStepSimplifier.Protocol;
@@ -123,7 +121,7 @@ public Statistics(List startNodes) {
blockLoopContractApps = tmp.block;
loopInvApps = tmp.inv;
autoModeTimeInMillis = startNode.proof().getAutoModeTime();
- timeInMillis = (System.currentTimeMillis() - startNode.proof().creationTime);
+ timeInMillis = (System.currentTimeMillis() - startNode.proof().getCreationTime());
}
this.nodes = nodes;
@@ -173,7 +171,7 @@ public Statistics(List startNodes) {
this.blockLoopContractApps = tmp.block;
this.loopInvApps = tmp.inv;
this.autoModeTimeInMillis = startNode.proof().getAutoModeTime();
- this.timeInMillis = (System.currentTimeMillis() - startNode.proof().creationTime);
+ this.timeInMillis = (System.currentTimeMillis() - startNode.proof().getCreationTime());
timePerStepInMillis = nodes <= 1 ? .0f : (autoModeTimeInMillis / (float) (nodes - 1));
generateSummary(startNode.proof());
@@ -183,7 +181,7 @@ public Statistics(List startNodes) {
this(proof.root());
}
- static Statistics create(Statistics side, long creationTime) {
+ protected static Statistics create(Statistics side, long creationTime) {
return new Statistics(side.nodes, side.branches, side.cachedBranches, side.interactiveSteps,
side.symbExApps,
side.quantifierInstantiations, side.ossApps, side.mergeRuleApps, side.totalRuleApps,
@@ -192,21 +190,8 @@ static Statistics create(Statistics side, long creationTime) {
System.currentTimeMillis() - creationTime, side.timePerStepInMillis);
}
- private void generateSummary(Proof proof) {
+ protected void generateSummary(Proof proof) {
Statistics stat = this;
-
- boolean sideProofs = false;
- if (proof instanceof InfFlowProof) { // TODO: get rid of that instanceof by subclassing
- sideProofs = ((InfFlowProof) proof).hasSideProofs();
- if (sideProofs) {
- final long autoTime = proof.getAutoModeTime()
- + ((InfFlowProof) proof).getSideProofStatistics().autoModeTimeInMillis;
- final SideProofStatistics side = ((InfFlowProof) proof).getSideProofStatistics()
- .add(this).setAutoModeTime(autoTime);
- stat = create(side, proof.creationTime);
- }
- }
-
final String nodeString = EnhancedStringBuffer.format(stat.nodes).toString();
summaryList.add(new Pair<>("Nodes", nodeString));
summaryList.add(new Pair<>("Branches",
@@ -219,8 +204,7 @@ private void generateSummary(Proof proof) {
summaryList.add(new Pair<>("Interactive steps", String.valueOf(stat.interactiveSteps)));
summaryList.add(new Pair<>("Symbolic execution steps", String.valueOf(stat.symbExApps)));
-
- final long time = sideProofs ? stat.autoModeTimeInMillis : proof.getAutoModeTime();
+ final long time = proof.getAutoModeTime();
summaryList.add(new Pair<>("Automode time",
EnhancedStringBuffer.formatTime(time).toString()));
@@ -270,11 +254,11 @@ public String toString() {
for (Pair p : summaryList) {
final String c = p.first;
final String s = p.second;
- sb = sb.append(c);
- if (!"".equals(s)) {
- sb = sb.append(": ").append(s);
+ sb.append(c);
+ if (!s.isEmpty()) {
+ sb.append(": ").append(s);
}
- sb = sb.append('\n');
+ sb.append('\n');
}
sb.deleteCharAt(sb.length() - 1);
return sb.toString();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java
index 45946f69fab..cc75770ea9b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java
@@ -456,7 +456,7 @@ public void readProblem() throws ProofInputException {
collectClassAxioms(getCalleeKeYJavaType(), proofConfig);
// for JML annotation statements
- generateWdTaclets(proofConfig);
+ generateDynamicTaclets(proofConfig);
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java
index ff5a76f5d08..3f2ef79bbeb 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java
@@ -19,7 +19,6 @@
import de.uka.ilkd.key.proof.mgt.AxiomJustification;
import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
import de.uka.ilkd.key.rule.NoPosTacletApp;
-import de.uka.ilkd.key.rule.RewriteTaclet;
import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.settings.Configuration;
import de.uka.ilkd.key.speclang.*;
@@ -94,52 +93,15 @@ private ImmutableSet getAxiomsForObserver(Pair}) or
- * WD(pv.m(...)).
- *
- * @param proofConfig the proof configuration
- */
- void generateWdTaclets(InitConfig proofConfig) {
- if (!WellDefinednessCheck.isOn()) {
- return;
- }
- ImmutableSet res = DefaultImmutableSet.nil();
- ImmutableSet names = DefaultImmutableSet.nil();
- for (WellDefinednessCheck ch : specRepos.getAllWdChecks()) {
- if (ch instanceof MethodWellDefinedness mwd) {
- // WD(callee.m(...))
- RewriteTaclet mwdTaclet = mwd.createOperationTaclet(proofConfig.getServices());
- String tName = mwdTaclet.name().toString();
- final String prefix;
- if (tName.startsWith(WellDefinednessCheck.OP_TACLET)) {
- prefix = WellDefinednessCheck.OP_TACLET;
- } else if (tName.startsWith(WellDefinednessCheck.OP_EXC_TACLET)) {
- prefix = WellDefinednessCheck.OP_EXC_TACLET;
- } else {
- prefix = "";
- }
- tName = tName.replace(prefix, "");
- if (names.contains(tName)) {
- for (RewriteTaclet t : res) {
- if (t.find().toString().equals(mwdTaclet.find().toString())) {
- res = res.remove(t);
- names = names.remove(tName);
- mwdTaclet = mwd.combineTaclets(t, mwdTaclet, proofConfig.getServices());
- }
- }
- }
- res = res.add(mwdTaclet);
- names = names.add(tName);
- }
- }
- // WD(a.)
- res = res.union(ClassWellDefinedness.createInvTaclet(proofConfig.getServices()));
- for (RewriteTaclet t : res) {
- register(t, proofConfig);
- }
+ /// Queries the registered (dynamic) taclet generators.
+ /// The taclet generator receives the `initConfig` to add further taclets to the proof.
+ /// @see TacletPOGenerator
+ protected void generateDynamicTaclets(InitConfig initConfig) {
+ var generators = ServiceLoader.load(TacletPOGenerator.class);
+ generators.forEach(it -> it.generate(this, initConfig, specRepos));
}
+
protected ImmutableSet selectClassAxioms(KeYJavaType selfKJT) {
return specRepos.getClassAxioms(selfKJT);
}
@@ -149,7 +111,7 @@ protected void collectClassAxioms(KeYJavaType selfKJT, InitConfig proofConfig) {
registerClassAxiomTaclets(selfKJT, proofConfig);
}
- private void register(Taclet t, InitConfig proofConfig) {
+ public void register(Taclet t, InitConfig proofConfig) {
assert t != null;
taclets = taclets.add(NoPosTacletApp.createNoPosTacletApp(t));
proofConfig.registerRule(t, AxiomJustification.INSTANCE);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractProfile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractProfile.java
index 83ac77ecdd7..ac730af8568 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractProfile.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractProfile.java
@@ -8,6 +8,7 @@
import de.uka.ilkd.key.logic.label.TermLabelManager.TermLabelConfiguration;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.io.RuleSource;
import de.uka.ilkd.key.proof.io.RuleSourceFactory;
import de.uka.ilkd.key.proof.mgt.AxiomJustification;
import de.uka.ilkd.key.proof.mgt.RuleJustification;
@@ -58,8 +59,8 @@ private static ImmutableSet extractNames(
}
protected AbstractProfile(String standardRuleFilename) {
- standardRules = new RuleCollection(
- RuleSourceFactory.fromDefaultLocation(standardRuleFilename), initBuiltInRules());
+ final var ruleSource = RuleSourceFactory.fromDefaultLocation(standardRuleFilename);
+ standardRules = new RuleCollection(ImmutableList.of(ruleSource), initBuiltInRules());
strategies = getStrategyFactories();
this.supportedGCB = computeSupportedGoalChooserBuilder();
this.supportedGC = extractNames(supportedGCB);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
index 214bac7e50d..d9cdb93db00 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
@@ -79,7 +79,7 @@ public FunctionalBlockContractPO(InitConfig initConfig, FunctionalBlockContract
* @param tb the TermBuilder to be used
* @return an anonymizing update for the specified variables.
*/
- private static JTerm createLocalAnonUpdate(
+ protected static JTerm createLocalAnonUpdate(
final ImmutableSet localOutVariables,
final Services services, final TermBuilder tb) {
JTerm localAnonUpdate = null;
@@ -198,7 +198,7 @@ private static JTerm[] createPostconditions(
* @param tb a term builder.
* @return the validity formula for the contract.
*/
- private static JTerm setUpValidityTerm(final List heaps,
+ protected JTerm setUpValidityTerm(final List heaps,
Map anonHeaps,
Map anonOutHeaps,
final ImmutableSet localInVariables,
@@ -211,46 +211,7 @@ private static JTerm setUpValidityTerm(final List heaps,
exceptionParameter, conditionsAndClausesBuilder.getTerms());
JTerm wellFormedAnonymisationHeapsCondition =
conditionsAndClausesBuilder.buildWellFormedAnonymisationHeapsCondition(anonHeaps);
- validity = tb.imp(tb.and(assumptions[1], wellFormedAnonymisationHeapsCondition), validity);
-
- return addWdToValidityTerm(validity, updates, heaps, anonOutHeaps, localInVariables,
- localOutVariables, bc, configurator, services, tb);
- }
-
- /**
- *
- * @param validity the validity formula.
- * @param updates the updates.
- * @param heaps the heaps.
- * @param anonOutHeaps the heaps used in the anonOut update.
- * @param localInVariables the free local variables in the block.
- * @param localOutVariables the free local variables modifiable by the block.
- * @param bc the contract being applied.
- * @param configurator a goal configurator
- * @param services services.
- * @param tb a term builder.
- * @return the conjunction of the well-definedness formula and the validity formula.
- */
- private static JTerm addWdToValidityTerm(JTerm validity, final JTerm[] updates,
- final List heaps, Map anonOutHeaps,
- final ImmutableSet localInVariables,
- final ImmutableSet localOutVariables, final BlockContract bc,
- final GoalsConfigurator configurator, final Services services, final TermBuilder tb) {
- if (WellDefinednessCheck.isOn()) {
- final JTerm wdUpdate = services.getTermBuilder().parallel(updates[1], updates[2]);
-
- JTerm localAnonUpdate = createLocalAnonUpdate(localOutVariables, services, tb);
-
- if (localAnonUpdate == null) {
- localAnonUpdate = tb.skip();
- }
-
- JTerm wellDefinedness = configurator.setUpWdGoal(null, bc, wdUpdate, localAnonUpdate,
- heaps.get(0), anonOutHeaps.get(heaps.get(0)), localInVariables);
-
- validity = tb.and(wellDefinedness, validity);
- }
- return validity;
+ return tb.imp(tb.and(assumptions[1], wellFormedAnonymisationHeapsCondition), validity);
}
@Override
@@ -361,7 +322,7 @@ public void readProblem() {
assignPOTerms(validity);
collectClassAxioms(getCalleeKeYJavaType(), proofConfig);
- generateWdTaclets(proofConfig);
+ generateDynamicTaclets(proofConfig);
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
index f51a06954e1..0f47c9b5a88 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
@@ -177,7 +177,7 @@ public void readProblem() {
assignPOTerms(validity);
collectClassAxioms(getCalleeKeYJavaType(), proofConfig);
- generateWdTaclets(proofConfig);
+ generateDynamicTaclets(proofConfig);
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/IPersistablePO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/IPersistablePO.java
index d9e490fac6c..bb83ea4f41c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/IPersistablePO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/IPersistablePO.java
@@ -4,8 +4,10 @@
package de.uka.ilkd.key.proof.init;
import java.io.IOException;
+import java.io.PrintWriter;
import java.util.Properties;
+import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.io.ProofSaver;
import de.uka.ilkd.key.settings.Configuration;
@@ -75,6 +77,20 @@ public interface IPersistablePO extends ProofOblInput {
*/
Configuration createLoaderConfig() throws IOException;
+ /// Called to manifest the proof manifest the proof obligation configuration
+ /// into the given {@link PrintWriter}
+ /// If the method returns `true`, a `\proofObligation` statement was successfully written
+ /// to the `ps`. Therefore, no `\problem` statement is printed.
+ ///
+ /// @return true if a `\proofObligation` was written successfully.
+ default boolean printProofObligation(PrintWriter ps, Proof proof) throws IOException {
+ var loadingConfig = createLoaderConfig();
+ ps.println("\\proofObligation ");
+ loadingConfig.save(ps, "");
+ ps.println("\n");
+ return true;
+ }
+
/**
* The class stored in a {@link Properties} instance via key must provide the static method with
* the following signature:
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java
index 3deea887e1a..6d00d372c2e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java
@@ -457,4 +457,13 @@ public FileRepo getFileRepo() {
public void setFileRepo(FileRepo fileRepo) {
this.fileRepo = fileRepo;
}
+
+ /// Enforce the given choice. Remove choices of the same category from the current set.
+ public void activateChoice(Choice choice) {
+ setActivatedChoices(
+ getActivatedChoices()
+ .stream().filter(it -> choice.category().equals(it.category()))
+ .collect(ImmutableSet.collector())
+ .add(choice));
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java
index d91cbbd771c..196c2bea5be 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java
@@ -11,6 +11,7 @@
import de.uka.ilkd.key.proof.mgt.ComplexRuleJustification;
import de.uka.ilkd.key.proof.mgt.ComplexRuleJustificationBySpec;
import de.uka.ilkd.key.proof.mgt.RuleJustification;
+import de.uka.ilkd.key.proof.rules.ComplexJustificationable;
import de.uka.ilkd.key.prover.impl.DepthFirstGoalChooserFactory;
import de.uka.ilkd.key.rule.*;
import de.uka.ilkd.key.rule.label.OriginTermLabelPolicy;
@@ -32,9 +33,31 @@
*
*/
public class JavaProfile extends AbstractProfile {
- public static final String NAME = "Java Profile";
+ public static final String PROFILE_ID = "Java Profile";
public static final String NAME_WITH_PERMISSIONS = "Java with Permissions Profile";
+ /**
+ * the name of the profile
+ *
+ * @return the name
+ */
+ @Override
+ public String ident() {
+ return permissions ? NAME_WITH_PERMISSIONS : PROFILE_ID;
+ }
+
+ @Override
+ public String displayName() {
+ return permissions ? NAME_WITH_PERMISSIONS : (PROFILE_ID + " (Default)");
+ }
+
+ @Override
+ public String description() {
+ return permissions
+ ? "Java programs with support for permissions"
+ : "The default for Java programs";
+ }
+
/**
*
* The default instance of this class.
@@ -181,23 +204,14 @@ public OneStepSimplifier getOneStepSimpilifier() {
*/
@Override
public RuleJustification getJustification(Rule r) {
- return r == UseOperationContractRule.INSTANCE || r == UseDependencyContractRule.INSTANCE
- || r == BlockContractExternalRule.INSTANCE || r == LoopContractExternalRule.INSTANCE
- ? new ComplexRuleJustificationBySpec()
- : super.getJustification(r);
+ if (r instanceof ComplexJustificationable) {
+ return new ComplexRuleJustificationBySpec();
+ } else {
+ return super.getJustification(r);
+ }
}
- /**
- * the name of the profile
- *
- * @return the name
- */
- @Override
- public String name() {
- return permissions ? NAME_WITH_PERMISSIONS : NAME;
- }
-
/**
* the default strategy factory to be used
*
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfileDefaultProfileResolver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfileDefaultProfileResolver.java
index 097cbfdd776..8d7d84e3fbe 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfileDefaultProfileResolver.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfileDefaultProfileResolver.java
@@ -14,7 +14,7 @@ public class JavaProfileDefaultProfileResolver implements DefaultProfileResolver
*/
@Override
public String getProfileName() {
- return JavaProfile.NAME;
+ return JavaProfile.PROFILE_ID;
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
index f8138c31c75..ce4d4e21368 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
@@ -438,14 +438,19 @@ public InitConfig prepare(EnvInput envInput) throws ProofInputException {
Profile profile = services.getProfile();
if (currentBaseConfig == null || profile != currentBaseConfig.getProfile()) {
currentBaseConfig = new InitConfig(services);
- RuleSource tacletBase = profile.getStandardRules().getTacletBase();
- if (tacletBase != null) {
- KeYFile tacletBaseFile = new KeYFile("taclet base",
- profile.getStandardRules().getTacletBase(), progMon, profile);
- readEnvInput(tacletBaseFile, currentBaseConfig);
+ ImmutableList tacletBases = profile.getStandardRules().getTacletBase();
+ if (tacletBases != null) {
+ for (var tacletBase : tacletBases) {
+ KeYFile tacletBaseFile = new KeYFile("taclet base (%s)".formatted(tacletBase.file().getFileName()),
+ tacletBase, progMon, profile);
+ readEnvInput(tacletBaseFile, currentBaseConfig);
+ }
}
// remove traces of the generic sorts within the base configuration
cleanupNamespaces(currentBaseConfig);
+
+ profile.prepareInitConfig(currentBaseConfig);
+
baseConfig = currentBaseConfig;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java
index f99c8047dbb..084e1fbb7f3 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java
@@ -3,13 +3,17 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.proof.init;
+import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.label.TermLabelManager;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.mgt.RuleJustification;
+import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
import de.uka.ilkd.key.rule.OneStepSimplifier;
import de.uka.ilkd.key.rule.Rule;
+import de.uka.ilkd.key.rule.UseDependencyContractRule;
+import de.uka.ilkd.key.rule.UseOperationContractRule;
import de.uka.ilkd.key.strategy.StrategyFactory;
-
+import org.jspecify.annotations.NonNull;
import org.key_project.logic.Name;
import org.key_project.prover.engine.GoalChooserFactory;
import org.key_project.prover.proof.ProofGoal;
@@ -17,8 +21,6 @@
import org.key_project.prover.rules.RuleApp;
import org.key_project.util.collection.ImmutableSet;
-import org.jspecify.annotations.NonNull;
-
/**
*
* This interface provides methods that allow to customize KeY for certain applications. It supports
@@ -29,7 +31,7 @@
*
the goal selection strategy
* the way how term labels are maintained
*
- *
+ *
* Currently this is only rudimentary: possible extensions are
*
* - program model to use (java, misrac, csharp)
@@ -38,7 +40,7 @@
* etc.
*
*
- * Each {@link Profile} has a unique name {@link #name()}.
+ * Each {@link Profile} has a unique name {@link #ident()}.
*
*
* It is recommended to have only one instance of each {@link Profile}. The default instances for
@@ -57,13 +59,31 @@
*/
public interface Profile {
- /** returns the rule source containg all taclets for this profile */
+ /**
+ * returns the rule source containg all taclets for this profile
+ */
RuleCollection getStandardRules();
- /** the name of this profile */
- String name();
+ /**
+ * the name of this profile used to for storing into key files, and for loading
+ */
+ String ident();
+
+ /**
+ * the name of this profile presentable for humans
+ */
+ default String displayName() {
+ return ident();
+ }
- /** returns the strategy factories for the supported strategies */
+ /// A description of this profile for the user
+ default String description() {
+ return "";
+ }
+
+ /**
+ * returns the strategy factories for the supported strategies
+ */
ImmutableSet supportedStrategies();
/**
@@ -109,7 +129,9 @@ public interface Profile {
*/
, G extends ProofGoal<@NonNull G>> GoalChooserFactory
getSelectedGoalChooserBuilder();
- /** returns the (default) justification for the given rule */
+ /**
+ * returns the (default) justification for the given rule
+ */
RuleJustification getJustification(Rule r);
@@ -130,4 +152,32 @@ public interface Profile {
TermLabelManager getTermLabelManager();
boolean isSpecificationInvolvedInRuleApp(RuleApp app);
+
+ /// Create an instance of a specification repository suitable for the given profile.
+ /// For example WD requires a special instance.
+ default SpecificationRepository createSpecificationRepository(Services services) {
+ return new SpecificationRepository(services);
+ }
+
+ /// Returns the implementation of a [UseDependencyContractRule] for this profile.
+ ///
+ /// @see de.uka.ilkd.key.proof.io.IntermediateProofReplayer
+ default UseDependencyContractRule getUseDependencyContractRule() {
+ return UseDependencyContractRule.INSTANCE;
+ }
+
+ /// Returns the implementation of a [UseOperationContractRule] for this profile
+ ///
+ /// @see de.uka.ilkd.key.proof.io.IntermediateProofReplayer
+ default UseOperationContractRule getUseOperationContractRule() {
+ return UseOperationContractRule.INSTANCE;
+ }
+
+ /// Let a profile visit a freshly created init profile. Allows the setting of properties after the
+ /// Taclet base has been loaded, but before Java sources are loaded or the environment is established.
+ ///
+ /// @see ProblemInitializer
+ default void prepareInitConfig(InitConfig baseConfig) {
+
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofOblInput.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofOblInput.java
index 62e86553680..c64a0e6d045 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofOblInput.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofOblInput.java
@@ -4,7 +4,9 @@
package de.uka.ilkd.key.proof.init;
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.ProofAggregate;
+import de.uka.ilkd.key.strategy.StrategyProperties;
/**
@@ -38,4 +40,11 @@ public interface ProofOblInput {
* if not available.
*/
KeYJavaType getContainerType();
+
+
+ /// A way to do some stuff before this obligation get stored by
+ /// [de.uka.ilkd.key.proof.io.ProofSaver].
+ default void prepareSave(StrategyProperties strategyProperties, Proof proof) {
+
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/RuleCollection.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/RuleCollection.java
index 2751a5b863e..cce2044d35c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/RuleCollection.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/RuleCollection.java
@@ -12,13 +12,13 @@
/**
* This class contains the standard rules provided by a profile.
*/
-public record RuleCollection(RuleSource standardTaclets,
+public record RuleCollection(ImmutableList standardTaclets,
ImmutableList standardBuiltInRules) {
/**
- * returns the rule source containg all taclets for this profile
+ * returns the rule source containing all taclets for this profile
*/
- public RuleSource getTacletBase() { return standardTaclets; }
+ public ImmutableList getTacletBase() { return standardTaclets; }
/**
* returns a list of all built in rules to be used
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/TacletPOGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/TacletPOGenerator.java
new file mode 100644
index 00000000000..340366aaf90
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/TacletPOGenerator.java
@@ -0,0 +1,15 @@
+/* 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.init;
+
+import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (1/1/26)
+ */
+public interface TacletPOGenerator {
+ void generate(AbstractPO abstractPO, InitConfig initConfig, SpecificationRepository specRepo);
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java
index 03c43de3c17..167aff7270c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java
@@ -98,7 +98,7 @@ public boolean hasErrors() {
/**
* The file or folder to load.
*/
- private final Path file;
+ private Path file;
/**
* The filename of the proof in the zipped file (null if file is not a proof bundle).
@@ -108,17 +108,17 @@ public boolean hasErrors() {
/**
* The optional class path entries to use.
*/
- private final List classPath;
+ private List classPath;
/**
* An optional boot class path.
*/
- private final Path bootClassPath;
+ private Path bootClassPath;
/**
* The global includes to use.
*/
- private final List includes;
+ private List includes;
/**
* The {@link ProblemLoaderControl} to use.
@@ -128,7 +128,7 @@ public boolean hasErrors() {
/**
* The {@link Profile} to use for new {@link Proof}s.
*/
- private final Profile profileOfNewProofs;
+ private Profile profileOfNewProofs;
/**
* {@code true} to call {@link ProblemLoaderControl#selectProofObligation(InitConfig)} if no
@@ -151,28 +151,28 @@ public boolean hasErrors() {
/**
* The instantiated {@link EnvInput} which describes the file to load.
*/
- private EnvInput envInput;
+ private @Nullable EnvInput envInput;
/**
* The instantiated {@link ProblemInitializer} used during the loading process.
*/
- private ProblemInitializer problemInitializer;
+ private @Nullable ProblemInitializer problemInitializer;
/**
* The instantiated {@link InitConfig} which provides access to the loaded source elements and
* specifications.
*/
- private InitConfig initConfig;
+ private @Nullable InitConfig initConfig;
/**
* The instantiate proof or {@code null} if no proof was instantiated during loading process.
*/
- private Proof proof;
+ private @Nullable Proof proof;
/**
* The {@link ReplayResult} if available or {@code null} otherwise.
*/
- private ReplayResult result;
+ private @Nullable ReplayResult result;
/**
* Whether warnings (generated when loading the proof) should be ignored
@@ -180,21 +180,19 @@ public boolean hasErrors() {
*/
private boolean ignoreWarnings = false;
+ // format: (expected, found)
/**
* Maps internal error codes of the parser to human readable strings. The integers refer to the
* common MismatchedTokenExceptions, where one token is expected and another is found. Both are
* usually only referred to by their internal code.
*/
- private final static Map, String> mismatchErrors;
- private final static Map missedErrors;
+ private static final Map, String> mismatchErrors = new HashMap<>();
+ private static final Map missedErrors = new HashMap<>();
static {
- // format: (expected, found)
- mismatchErrors = new HashMap<>();
mismatchErrors.put(new Pair<>(KeYLexer.SEMI, KeYLexer.COMMA),
"there may be only one declaration per line");
- missedErrors = new HashMap<>();
missedErrors.put(KeYLexer.RPAREN, "closing parenthesis");
missedErrors.put(KeYLexer.RBRACE, "closing brace");
missedErrors.put(KeYLexer.SEMI, "semicolon");
@@ -226,8 +224,8 @@ protected AbstractProblemLoader(Path file, List classPath, Path bootClassP
this.classPath = classPath;
this.bootClassPath = bootClassPath;
this.control = control;
- this.profileOfNewProofs =
- profileOfNewProofs != null ? profileOfNewProofs : AbstractProfile.getDefaultProfile();
+ setProfileOfNewProofs(
+ profileOfNewProofs != null ? profileOfNewProofs : AbstractProfile.getDefaultProfile());
this.forceNewProfileOfNewProofs = forceNewProfileOfNewProofs;
this.askUiToSelectAProofObligationIfNotDefinedByLoadedFile =
askUiToSelectAProofObligationIfNotDefinedByLoadedFile;
@@ -235,7 +233,79 @@ protected AbstractProblemLoader(Path file, List classPath, Path bootClassP
this.includes = includes;
}
- protected void setProof(Proof proof) {
+ public void setFile(Path file) {
+ this.file = file;
+ }
+
+ public void setClassPath(@Nullable List classPath) {
+ this.classPath = classPath;
+ }
+
+ public void setBootClassPath(@Nullable Path bootClassPath) {
+ this.bootClassPath = bootClassPath;
+ }
+
+ public void setIncludes(@Nullable List includes) {
+ this.includes = includes;
+ }
+
+ public void setProofFilename(Path proofFilename) {
+ this.proofFilename = proofFilename;
+ }
+
+ public void setEnvInput(EnvInput envInput) {
+ this.envInput = envInput;
+ }
+
+ public void setProblemInitializer(ProblemInitializer problemInitializer) {
+ this.problemInitializer = problemInitializer;
+ }
+
+ public void setInitConfig(InitConfig initConfig) {
+ this.initConfig = initConfig;
+ }
+
+ public void setResult(ReplayResult result) {
+ this.result = result;
+ }
+
+ public Path getProofFilename() {
+ return proofFilename;
+ }
+
+ public List getIncludes() {
+ return includes;
+ }
+
+ public ProblemLoaderControl getControl() {
+ return control;
+ }
+
+ public Profile getProfileOfNewProofs() {
+ return profileOfNewProofs;
+ }
+
+ public void setProfileOfNewProofs(Profile profileOfNewProofs) {
+ this.profileOfNewProofs = profileOfNewProofs;
+ }
+
+ public boolean isAskUiToSelectAProofObligationIfNotDefinedByLoadedFile() {
+ return askUiToSelectAProofObligationIfNotDefinedByLoadedFile;
+ }
+
+ public Properties getPoPropertiesToForce() {
+ return poPropertiesToForce;
+ }
+
+ public boolean isForceNewProfileOfNewProofs() {
+ return forceNewProfileOfNewProofs;
+ }
+
+ public boolean isIgnoreWarnings() {
+ return ignoreWarnings;
+ }
+
+ protected void setProof(@Nullable Proof proof) {
this.proof = proof;
}
@@ -261,8 +331,7 @@ public final void load() throws Exception {
* @throws IOException Occurred Exception.
* @throws ProblemLoaderException Occurred Exception.
*/
- public final void load(Consumer callbackProofLoaded)
- throws Exception {
+ public final void load(Consumer callbackProofLoaded) throws Exception {
control.loadingStarted(this);
loadEnvironment();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
index e118c87a747..4e8e558ab5a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
@@ -281,7 +281,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
if (appInterm instanceof MergeAppIntermediate joinAppInterm) {
HashSet partnerNodesInfo =
- joinPartnerNodes.get(((MergeAppIntermediate) appInterm).getId());
+ joinPartnerNodes.get(joinAppInterm.getId());
if (partnerNodesInfo == null
|| partnerNodesInfo.size() < joinAppInterm.getNrPartners()) {
@@ -366,9 +366,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
addChildren(children, intermChildren);
} catch (SkipSMTRuleException e) {
- // silently continue; status will be reported
- // via
- // polling
+ // silently continue; status will be reported via polling
} catch (BuiltInConstructionException | AssertionError
| RuntimeException e) {
reportError(ERROR_LOADING_PROOF_LINE + "Line "
@@ -603,7 +601,9 @@ private IBuiltInRuleApp constructBuiltinApp(BuiltInAppIntermediate currInterm, G
}
}
- if (SMTRuleApp.RULE.name().toString().equals(ruleName)) {
+ final SMTRule smtRule = SMTRule.INSTANCE; // proof.getServices().getProfile().findInstanceFor(SMTRule.class);
+
+ if (smtRule.name().toString().equals(ruleName)) {
if (!ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings().isEnableOnLoad()) {
status = SMT_NOT_RUN;
throw new SkipSMTRuleException();
@@ -650,14 +650,14 @@ private IBuiltInRuleApp constructBuiltinApp(BuiltInAppIntermediate currInterm, G
ImmutableList unsatCore =
SMTFocusResults.getUnsatCore(smtProblem);
if (unsatCore != null) {
- return SMTRuleApp.RULE.createApp(name, unsatCore);
+ return smtRule.createApp(name, unsatCore);
} else {
- return SMTRuleApp.RULE.createApp(name);
+ return smtRule.createApp(name);
}
}
}
- IBuiltInRuleApp ourApp = null;
+ IBuiltInRuleApp ourApp;
PosInOccurrence pos = null;
if (currFormula != 0) { // otherwise we have no pos
@@ -670,19 +670,16 @@ private IBuiltInRuleApp constructBuiltinApp(BuiltInAppIntermediate currInterm, G
}
if (currContract != null) {
- AbstractContractRuleApp contractApp = null;
+ AbstractContractRuleApp> contractApp;
- BuiltInRule useContractRule;
if (currContract instanceof OperationContract) {
- useContractRule = UseOperationContractRule.INSTANCE;
- contractApp = (((UseOperationContractRule) useContractRule).createApp(pos))
- .setContract(currContract);
+ var rule = proof.getServices().getProfile().getUseOperationContractRule();
+ contractApp = rule.createApp(pos).setContract(currContract);
} else {
- useContractRule = UseDependencyContractRule.INSTANCE;
- contractApp = (((UseDependencyContractRule) useContractRule).createApp(pos))
- .setContract(currContract);
+ var rule = proof.getServices().getProfile().getUseDependencyContractRule();
+ contractApp = rule.createApp(pos).setContract(currContract);
// restore "step" if needed
- var depContractApp = ((UseDependencyContractApp) contractApp);
+ var depContractApp = ((UseDependencyContractApp>) contractApp);
if (depContractApp.step() == null) {
contractApp = depContractApp.setStep(builtinIfInsts.head());
}
@@ -694,10 +691,8 @@ private IBuiltInRuleApp constructBuiltinApp(BuiltInAppIntermediate currInterm, G
ourApp = contractApp;
}
- currContract = null;
if (builtinIfInsts != null) {
ourApp = ourApp.setAssumesInsts(builtinIfInsts);
- builtinIfInsts = null;
}
return ourApp;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java
index 0db5b7fd9f5..270be48fe28 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java
@@ -10,9 +10,6 @@
import de.uka.ilkd.key.axiom_abstraction.AbstractDomainElement;
import de.uka.ilkd.key.axiom_abstraction.predicateabstraction.AbstractionPredicate;
-import de.uka.ilkd.key.informationflow.po.AbstractInfFlowPO;
-import de.uka.ilkd.key.informationflow.po.InfFlowCompositePO;
-import de.uka.ilkd.key.informationflow.proof.InfFlowProof;
import de.uka.ilkd.key.java.ProgramElement;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.*;
@@ -59,6 +56,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;
@@ -90,14 +88,14 @@ public class OutputStreamProofSaver {
* @param proof the Proof
* @return the location of the java source code or null if no such exists
*/
- public static File getJavaSourceLocation(Proof proof) {
+ public static @Nullable File getJavaSourceLocation(Proof proof) {
final String header = proof.header();
final int i = header.indexOf("\\javaSource");
if (i >= 0) {
final int begin = header.indexOf('\"', i);
final int end = header.indexOf('\"', begin + 1);
final String sourceLocation = header.substring(begin + 1, end);
- if (sourceLocation.length() > 0) {
+ if (!sourceLocation.isEmpty()) {
return new File(sourceLocation);
}
}
@@ -153,7 +151,7 @@ public StringBuffer writeLog() {
}
public String writeProfile(Profile profile) {
- return "\\profile \"" + escapeCharacters(profile.name()) + "\";\n";
+ return "\\profile \"" + escapeCharacters(profile.ident()) + "\";\n";
}
public String writeSettings(ProofSettings ps) {
@@ -174,47 +172,42 @@ public void save(OutputStream out) throws IOException {
final StrategySettings strategySettings = proof.getSettings().getStrategySettings();
final StrategyProperties strategyProperties =
strategySettings.getActiveStrategyProperties();
- if (po instanceof AbstractInfFlowPO && (po instanceof InfFlowCompositePO
- || !((InfFlowProof) proof).getIFSymbols().isFreshContract())) {
- strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY,
- StrategyProperties.INF_FLOW_CHECK_TRUE);
- strategySettings.setActiveStrategyProperties(strategyProperties);
- for (final SequentFormula s : proof.root().sequent()
- .succedent().asList()) {
- ((InfFlowProof) proof).addLabeledTotalTerm((JTerm) s.formula());
- }
- } else {
- strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY,
- StrategyProperties.INF_FLOW_CHECK_FALSE);
- strategySettings.setActiveStrategyProperties(strategyProperties);
+
+ if (po != null) {
+ // synthetic proofs (e.g., generated by test cases) do not necessary have proof
+ // obligations.
+ po.prepareSave(strategyProperties, proof);
}
+
+ // FIXME weigl
+ // strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY,
+ // StrategyProperties.INF_FLOW_CHECK_FALSE);
+ strategySettings.setActiveStrategyProperties(strategyProperties);
ps.println(writeSettings(proof.getSettings()));
- if (po instanceof AbstractInfFlowPO && (po instanceof InfFlowCompositePO
- || !((InfFlowProof) proof).getIFSymbols().isFreshContract())) {
- strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY,
- StrategyProperties.INF_FLOW_CHECK_FALSE);
- strategySettings.setActiveStrategyProperties(strategyProperties);
- }
+ /*
+ * FIXME weigl
+ * if (po instanceof AbstractInfFlowPO && (po instanceof InfFlowCompositePO
+ * || !((InfFlowProof) proof).getIFSymbols().isFreshContract())) {
+ * strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY,
+ * StrategyProperties.INF_FLOW_CHECK_FALSE);
+ * strategySettings.setActiveStrategyProperties(strategyProperties);
+ */
// declarations of symbols, sorts
+ // FIXME this should rather be an AST rewrite, than a bunch of regex.
String header = proof.header();
header = makePathsRelative(header);
ps.print(header);
+ proof.printSymbols(ps);
+
// \problem or \proofObligation
- if (po instanceof IPersistablePO ppo
- && (!(po instanceof AbstractInfFlowPO) || (!(po instanceof InfFlowCompositePO)
- && ((InfFlowProof) proof).getIFSymbols().isFreshContract()))) {
- var loadingConfig = ppo.createLoaderConfig();
- ps.println("\\proofObligation ");
- loadingConfig.save(ps, "");
- ps.println("\n");
- } else {
- if (po instanceof AbstractInfFlowPO && (po instanceof InfFlowCompositePO
- || !((InfFlowProof) proof).getIFSymbols().isFreshContract())) {
- ps.print(((InfFlowProof) proof).printIFSymbols());
- }
+ var hasProofObligation =
+ po instanceof IPersistablePO ppo && ppo.printProofObligation(ps, proof);
+
+
+ if (!hasProofObligation) {
final Sequent problemSeq = proof.root().sequent();
ps.println("\\problem {");
if (problemSeq.antecedent().isEmpty() && problemSeq.succedent().size() == 1) {
@@ -239,7 +232,7 @@ public void save(OutputStream out) throws IOException {
}
}
- protected Path getBasePath() throws IOException {
+ protected @Nullable Path getBasePath() throws IOException {
File javaSourceLocation = getJavaSourceLocation(proof);
if (javaSourceLocation != null) {
return javaSourceLocation.toPath().toAbsolutePath();
@@ -472,7 +465,7 @@ private void printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp, Node node
// Predicates for merges with predicate abstraction.
if (concreteRule instanceof MergeWithPredicateAbstraction
- && ((MergeWithPredicateAbstraction) concreteRule).getPredicates().size() > 0) {
+ && !((MergeWithPredicateAbstraction) concreteRule).getPredicates().isEmpty()) {
printPredicatesForSingleMergeRuleApp((MergeWithPredicateAbstraction) concreteRule,
output);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ComplexRuleJustificationBySpec.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ComplexRuleJustificationBySpec.java
index 0184a0a2c32..fd56a61c99e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ComplexRuleJustificationBySpec.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ComplexRuleJustificationBySpec.java
@@ -12,9 +12,7 @@
public class ComplexRuleJustificationBySpec implements ComplexRuleJustification {
- private final Map app2Just =
- new LinkedHashMap<>();
-
+ private final Map app2Just = new LinkedHashMap<>();
@Override
public boolean isAxiomJustification() {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java
index 34651c4fa3c..ac92d023781 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java
@@ -6,7 +6,6 @@
import java.util.LinkedHashMap;
import java.util.Map;
-import de.uka.ilkd.key.informationflow.rule.InfFlowContractAppTaclet;
import de.uka.ilkd.key.rule.RuleKey;
import org.key_project.logic.LogicServices;
@@ -51,9 +50,10 @@ public void addJustification(Rule r, RuleJustification j) {
}
public void removeJustificationFor(Rule rule) {
- if (InfFlowContractAppTaclet.hasType(rule)) {
- InfFlowContractAppTaclet.unregister(rule.name());
- }
+ // FIXME weigl: Unclear why this is needed
+ // if (InfFlowContractAppTaclet.hasType(rule)) {
+ // InfFlowContractAppTaclet.unregister(rule.name());
+ // }
rule2Justification.remove(new RuleKey(rule));
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
index f907dd51fee..a75a4bcffa0 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
@@ -41,11 +41,7 @@
import org.key_project.prover.rules.RuleSet;
import org.key_project.prover.sequent.Sequent;
import org.key_project.prover.sequent.SequentFormula;
-import org.key_project.util.collection.DefaultImmutableSet;
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
-import org.key_project.util.collection.ImmutableSet;
-import org.key_project.util.collection.Pair;
+import org.key_project.util.collection.*;
import org.jspecify.annotations.Nullable;
import org.slf4j.Logger;
@@ -56,7 +52,7 @@
* invariants. Provides methods for adding such elements to the repository, and for retrieving them
* afterwards.
*/
-public final class SpecificationRepository {
+public class SpecificationRepository {
private static final Logger LOGGER = LoggerFactory.getLogger(SpecificationRepository.class);
public static final String CONTRACT_COMBINATION_MARKER = "#";
@@ -70,17 +66,15 @@ public final class SpecificationRepository {
private final ContractFactory cf;
- private final Map, ImmutableSet> contracts =
+ protected final Map, ImmutableSet> contracts =
new LinkedHashMap<>();
- private final Map, ImmutableSet> operationContracts =
+ protected final Map, ImmutableSet> operationContracts =
new LinkedHashMap<>();
- private final Map, ImmutableSet> wdChecks =
- new LinkedHashMap<>();
- private final Map contractsByName = new LinkedHashMap<>();
- private final Map> contractTargets =
+ protected final Map contractsByName = new LinkedHashMap<>();
+ protected final Map> contractTargets =
new LinkedHashMap<>();
private final Map> invs = new LinkedHashMap<>();
- private final Map> axioms = new LinkedHashMap<>();
+ protected final Map> axioms = new LinkedHashMap<>();
private final Map> initiallyClauses =
new LinkedHashMap<>();
private final Map> proofs = new LinkedHashMap<>();
@@ -120,8 +114,8 @@ public final class SpecificationRepository {
private final Map> allClassAxiomsCache =
new LinkedHashMap<>();
- private final Services services;
- private final TermBuilder tb;
+ protected final Services services;
+ protected final TermBuilder tb;
private final Map contractCounters =
new de.uka.ilkd.key.util.LinkedHashMap<>();
@@ -219,7 +213,7 @@ private static JModality.JavaModalityKind getMatchModalityKind(
}
}
- private IObserverFunction getCanonicalFormForKJT(IObserverFunction obs, KeYJavaType kjt) {
+ protected IObserverFunction getCanonicalFormForKJT(IObserverFunction obs, KeYJavaType kjt) {
assert obs != null;
assert kjt != null;
if (!(obs instanceof IProgramMethod pm) || obs.getContainerType().equals(kjt)) {
@@ -371,7 +365,7 @@ assert getCanonicalFormForKJT(contract.getTarget(), contract.getKJT())
return contract;
}
- private void registerContract(Contract contract) {
+ protected void registerContract(Contract contract) {
final Pair target =
new Pair<>(contract.getKJT(), contract.getTarget());
registerContract(contract, target);
@@ -384,80 +378,42 @@ private void registerContract(Contract contract,
}
}
- private void registerContract(Contract contract,
+ protected void registerContract(Contract contract,
Pair targetPair) {
LOGGER.trace("Contract registered {}", contract);
- if (!WellDefinednessCheck.isOn() && contract instanceof WellDefinednessCheck) {
- return;
- }
final KeYJavaType targetKJT = targetPair.first;
final IObserverFunction targetMethod = targetPair.second;
contract = contract.setTarget(targetKJT, targetMethod);
final String name = contract.getName();
- assert contractsByName.get(name) == null
- : "Tried to add a contract with a non-unique name: " + name;
+ if (contractsByName.get(name) != null) {
+ LOGGER.error("Tried to add a contract with a non-unique name: {}", name);
+ // throw new IllegalStateException("Tried to add a contract with a non-unique name: " +
+ // name);
+ return;
+ }
assert !name.contains(CONTRACT_COMBINATION_MARKER)
: "Tried to add a contract with a name containing the" + " reserved character "
+ CONTRACT_COMBINATION_MARKER + ": " + name;
assert contract.id() != Contract.INVALID_ID : "Tried to add a contract with an invalid id!";
contracts.put(targetPair, getContracts(targetKJT, targetMethod).add(contract));
- if (contract instanceof FunctionalOperationContract) {
- operationContracts.put(new Pair<>(targetKJT, (IProgramMethod) targetMethod),
- getOperationContracts(targetKJT, (IProgramMethod) targetMethod)
- .add((FunctionalOperationContract) contract));
- // Create new well-definedness check
- final MethodWellDefinedness mwd =
- new MethodWellDefinedness((FunctionalOperationContract) contract, services);
- registerContract(mwd);
- } else if (contract instanceof DependencyContract && contract.getOrigVars().atPres.isEmpty()
- && targetMethod.getContainerType()
- .equals(services.getJavaInfo().getJavaLangObject())) {
- // Create or extend a well-definedness check for a class invariant
- final JTerm deps =
- contract.getAccessible(services.getTypeConverter().getHeapLDT().getHeap());
- final JTerm mby = contract.getMby();
- final String invName = "JML model class invariant in " + targetKJT.getName();
- final ClassInvariant inv = new ClassInvariantImpl(invName, invName, targetKJT,
- contract.getVisibility(), tb.tt(), contract.getOrigVars().self);
- ClassWellDefinedness cwd =
- new ClassWellDefinedness(inv, targetMethod, deps, mby, services);
- final ImmutableSet cwds = getWdClassChecks(targetKJT);
- if (!cwds.isEmpty()) {
- assert cwds.size() == 1;
- final ClassWellDefinedness oldCwd = cwds.iterator().next();
- unregisterContract(oldCwd);
- oldCwd.addInv(cwd.getInvariant().getInv(oldCwd.getOrigVars().self, services));
- cwd = oldCwd.combine(cwd, services);
- }
- registerContract(cwd);
- } else if (contract instanceof DependencyContract
- && contract.getOrigVars().atPres.isEmpty()) {
- // Create or extend a well-definedness check for a model field
- MethodWellDefinedness mwd =
- new MethodWellDefinedness((DependencyContract) contract, services);
- final ImmutableSet mwds =
- getWdMethodChecks(targetKJT, targetMethod);
- if (!mwds.isEmpty()) {
- assert mwds.size() == 1;
- final MethodWellDefinedness oldMwd = mwds.iterator().next();
- unregisterContract(oldMwd);
- mwd = mwd.combine(oldMwd, services);
- }
- registerContract(mwd);
- } else if (contract instanceof WellDefinednessCheck) {
- registerWdCheck((WellDefinednessCheck) contract);
- }
contractsByName.put(contract.getName(), contract);
final ImmutableSet oldTargets = getContractTargets(targetKJT);
final ImmutableSet newTargets = oldTargets.add(targetMethod);
contractTargets.put(targetKJT, newTargets);
+
+ // Special treatment
+ if (contract instanceof FunctionalOperationContract operationContract) {
+ operationContracts.put(new Pair<>(targetKJT, (IProgramMethod) targetMethod),
+ getOperationContracts(targetKJT, (IProgramMethod) targetMethod)
+ .add(operationContract));
+ }
}
/**
* Removes the contract from the repository, but keeps its target.
*/
- private void unregisterContract(Contract contract) {
+ protected void unregisterContract(Contract contract) {
final KeYJavaType kjt = contract.getKJT();
final Pair tp = new Pair<>(kjt, contract.getTarget());
contracts.put(tp, contracts.get(tp).remove(contract));
@@ -466,19 +422,6 @@ private void unregisterContract(Contract contract) {
new Pair<>(tp.first, (IProgramMethod) tp.second);
operationContracts.put(tp2,
operationContracts.get(tp2).remove((FunctionalOperationContract) contract));
- if (!getWdChecks(contract.getKJT(), contract.getTarget()).isEmpty()) {
- ImmutableSet wdcs =
- getWdChecks(contract.getKJT(), contract.getTarget());
- for (WellDefinednessCheck wdc : wdcs) {
- if (wdc instanceof MethodWellDefinedness
- && ((MethodWellDefinedness) wdc).getMethodContract().equals(contract)) {
- unregisterWdCheck(wdc);
- }
- }
- }
- }
- if (contract instanceof WellDefinednessCheck) {
- unregisterWdCheck((WellDefinednessCheck) contract);
}
contractsByName.remove(contract.getName());
}
@@ -509,8 +452,8 @@ private void createContractsFromInitiallyClause(InitiallyClause inv, KeYJavaType
if (oldFuncContracts.isEmpty()) {
final FunctionalOperationContract iniContr = cf.func(pm, inv);
addContractNoInheritance(iniContr);
- assert getContracts(kjt, pm).size() == (WellDefinednessCheck.isOn() ? 2 : 1)
- + oldContracts.size();
+ // assert getContracts(kjt, pm).size() == (WellDefinednessCheck.isOn() ? 2 : 1)
+ // + oldContracts.size();
} else {
for (FunctionalOperationContract c : oldFuncContracts) {
unregisterContract(c);
@@ -525,132 +468,6 @@ assert getContracts(kjt, pm).size() == (WellDefinednessCheck.isOn() ? 2 : 1)
// Internal interface for well-definedness checks
- /**
- * Remove well-definedness checks from a given set of contracts
- *
- * @param contracts A set of contracts
- * @return contracts without well-definedness checks
- */
- private static ImmutableSet removeWdChecks(ImmutableSet contracts) {
- ImmutableList result = ImmutableSLList.nil();
- if (contracts == null) {
- return contracts;
- }
- for (Contract c : contracts) {
- if (!(c instanceof WellDefinednessCheck)) {
- result = result.prepend(c);
- }
- }
- return DefaultImmutableSet.fromImmutableList(result);
- }
-
- /**
- * Registers a well-definedness check. It does not take care of its visibility in the proof
- * management dialog (this is done in {@link #registerContract(Contract, Pair)}).
- *
- * @param check The well-definedness check to be registered
- */
- private void registerWdCheck(WellDefinednessCheck check) {
- ImmutableSet checks =
- getWdChecks(check.getKJT(), check.getTarget()).add(check);
- wdChecks.put(new Pair<>(check.getKJT(), check.getTarget()), checks);
- }
-
- /**
- * Unregisters a well-definedness check. It does not take care of its visibility in the proof
- * management dialog.
- *
- * @param check The well-definedness check to be unregistered
- */
- private void unregisterWdCheck(WellDefinednessCheck check) {
- wdChecks.put(new Pair<>(check.getKJT(), check.getTarget()),
- getWdChecks(check.getKJT(), check.getTarget()).remove(check));
- }
-
- /**
- * Returns all registered (atomic) well-definedness checks for the passed kjt.
- */
- private ImmutableSet getWdChecks(KeYJavaType kjt) {
- assert kjt != null;
- ImmutableSet result = DefaultImmutableSet.nil();
- for (WellDefinednessCheck ch : getAllWdChecks()) {
- if (ch.getKJT().equals(kjt)) {
- result = result.add(ch);
- }
- }
- return result;
- }
-
- /**
- * Returns all registered (atomic) well-definedness checks for the passed target and kjt.
- */
- private ImmutableSet getWdChecks(KeYJavaType kjt,
- IObserverFunction target) {
- assert kjt != null;
- assert target != null;
- target = getCanonicalFormForKJT(target, kjt);
- final Pair pair = new Pair<>(kjt, target);
- final ImmutableSet result = wdChecks.get(pair);
- return result == null ? DefaultImmutableSet.nil() : result;
- }
-
- /**
- * Returns all registered well-definedness checks for method contracts.
- */
- private ImmutableSet getAllWdMethodChecks() {
- ImmutableSet result = DefaultImmutableSet.nil();
- for (var s : getAllWdChecks()) {
- if (s instanceof MethodWellDefinedness) {
- result = result.add((MethodWellDefinedness) s);
- }
- }
- return result;
- }
-
- /**
- * Returns all registered (atomic) well-definedness method checks for the passed kjt.
- */
- private ImmutableSet