wip

Author: wadoon

key.core/build.gradle

@@ -19,6 +19,8 @@ dependencies {
 
     antlr4 "org.antlr:antlr4:4.13.2"
     api "org.antlr:antlr4-runtime:4.13.2"
+
+    compileOnly "com.google.auto.service:auto-service:1.1.1"
 }
 
 // The target directory for JavaCC (parser generation)

…bFormulaOfInfFlowContractAppFeature.java …bFormulaOfInfFlowContractAppFeature.javakey.core/src/main/java/de/uka/ilkd/key/strategy/feature/FocusIsSubFormulaOfInfFlowContractAppFeature.java renamed to key.core/src/main/java/de/uka/ilkd/key/informationflow/FocusIsSubFormulaOfInfFlowContractAppFeature.java key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FocusIsSubFormulaOfInfFlowContractAppFeature.java renamed to key.core/src/main/java/de/uka/ilkd/key/informationflow/FocusIsSubFormulaOfInfFlowContractAppFeature.java

@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.strategy.feature;
+package de.uka.ilkd.key.informationflow;
 
 import de.uka.ilkd.key.informationflow.rule.executor.InfFlowContractAppTacletExecutor;
 import de.uka.ilkd.key.logic.DefaultVisitor;

…y/feature/InfFlowContractAppFeature.java …ationflow/InfFlowContractAppFeature.javakey.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java renamed to key.core/src/main/java/de/uka/ilkd/key/informationflow/InfFlowContractAppFeature.java key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java renamed to key.core/src/main/java/de/uka/ilkd/key/informationflow/InfFlowContractAppFeature.java

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

key.core/src/main/java/de/uka/ilkd/key/informationflow/InfFlowProfileResolver.java

@@ -0,0 +1,19 @@
+/* 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 de.uka.ilkd.key.proof.init.DefaultProfileResolver;
+import de.uka.ilkd.key.proof.init.Profile;
+
+public class InfFlowProfileResolver implements DefaultProfileResolver {
+    @Override
+    public String getProfileName() {
+        return "java-infflow";
+    }
+
+    @Override
+    public Profile getDefaultProfile() {
+        return new JavaInfFlowProfile();
+    }
+}

…ey/speclang/InformationFlowContract.java …rmationflow/InformationFlowContract.javakey.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContract.java renamed to key.core/src/main/java/de/uka/ilkd/key/informationflow/InformationFlowContract.java key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContract.java renamed to key.core/src/main/java/de/uka/ilkd/key/informationflow/InformationFlowContract.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.informationflow;
 
 import java.util.function.UnaryOperator;
 
@@ -11,6 +11,7 @@
 import de.uka.ilkd.key.logic.op.IObserverFunction;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
 import de.uka.ilkd.key.logic.op.JModality;
+import de.uka.ilkd.key.speclang.Contract;
 import de.uka.ilkd.key.util.InfFlowSpec;
 
 import org.key_project.util.collection.ImmutableList;

key.core/src/main/java/de/uka/ilkd/key/informationflow/JavaInfFlowProfile.java

@@ -0,0 +1,28 @@
+/* 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 de.uka.ilkd.key.informationflow.rule.InfFlowBlockContractInternalRule;
+import de.uka.ilkd.key.proof.init.JavaProfile;
+import de.uka.ilkd.key.rule.*;
+
+import org.key_project.util.collection.ImmutableList;
+
+/**
+ * This profile sets up KeY for verification of JavaCard programs.
+ */
+public class JavaInfFlowProfile extends JavaProfile {
+    public static final String NAME = "Java InfFlow Profile";
+
+    @Override
+    protected ImmutableList<BuiltInRule> initBuiltInRules() {
+        var rules = super.initBuiltInRules();
+        return rules.map(it -> {
+            if (it == BlockContractInternalRule.INSTANCE) {
+                return InfFlowBlockContractInternalRule.INSTANCE;
+            }
+            return it;
+        });
+    }
+}

…peclang/InformationFlowContractImpl.java …ow/impl/InformationFlowContractImpl.javakey.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java renamed to key.core/src/main/java/de/uka/ilkd/key/informationflow/impl/InformationFlowContractImpl.java key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java renamed to key.core/src/main/java/de/uka/ilkd/key/informationflow/impl/InformationFlowContractImpl.java

@@ -1,13 +1,14 @@
 /* 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.informationflow.impl;
 
 import java.util.Iterator;
 import java.util.List;
 import java.util.Map;
 import java.util.function.UnaryOperator;
 
+import de.uka.ilkd.key.informationflow.InformationFlowContract;
 import de.uka.ilkd.key.informationflow.po.InfFlowContractPO;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
@@ -21,6 +22,8 @@
 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.speclang.Contract;
+import de.uka.ilkd.key.speclang.ContractFactory;
 import de.uka.ilkd.key.util.InfFlowSpec;
 
 import org.key_project.util.collection.ImmutableList;

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/AbstractFinishAuxiliaryComputationMacro.java

@@ -32,7 +32,7 @@
  *
  * @author christoph
  */
-public abstract class AbstractFinishAuxiliaryComputationMacro extends AbstractProofMacro {
+abstract class AbstractFinishAuxiliaryComputationMacro extends AbstractProofMacro {
 
     @Override
     public String getName() {

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/FinishAuxiliaryMethodComputationMacro.java

@@ -4,6 +4,7 @@
 package de.uka.ilkd.key.informationflow.macros;
 
 import de.uka.ilkd.key.control.UserInterfaceControl;
+import de.uka.ilkd.key.informationflow.InformationFlowContract;
 import de.uka.ilkd.key.informationflow.po.IFProofObligationVars;
 import de.uka.ilkd.key.informationflow.po.InfFlowContractPO;
 import de.uka.ilkd.key.informationflow.po.SymbolicExecutionPO;
@@ -17,7 +18,6 @@
 import de.uka.ilkd.key.proof.init.ProofOblInput;
 import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
-import de.uka.ilkd.key.speclang.InformationFlowContract;
 
 import org.key_project.prover.engine.ProverTaskListener;
 import org.key_project.prover.sequent.PosInOccurrence;

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/FullInformationFlowAutoPilotMacro.java

@@ -87,7 +87,7 @@ protected ProofMacro[] createProofMacroArray() {
             public String getDescription() { return "Anonymous Macro"; }
         };
 
-        final AlternativeMacro alternativesMacro = new AlternativeMacro() {
+        return new AlternativeMacro() {
             @Override
             public String getName() { return ""; }
 
@@ -103,8 +103,6 @@ protected ProofMacro[] createProofMacroArray() {
                     finishMainCompMacro };
             }
         };
-
-        return alternativesMacro;
     }
 
     @Override