Taclet definition added to problemHeader

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/AbstractInfFlowPO.java

@@ -9,6 +9,7 @@
 import de.uka.ilkd.key.informationflow.proof.InfFlowCheckInfo;
 import de.uka.ilkd.key.informationflow.proof.InfFlowProof;
 import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.StrategyInfoUndoMethod;
 import de.uka.ilkd.key.proof.init.AbstractOperationPO;
@@ -18,6 +19,7 @@
 
 import org.key_project.prover.sequent.SequentFormula;
 
+import org.jspecify.annotations.Nullable;
 import org.slf4j.LoggerFactory;
 
 import static de.uka.ilkd.key.informationflow.proof.InfFlowCheckInfo.INF_FLOW_CHECK_TRUE;
@@ -45,7 +47,8 @@ public Proof createProof(String proofName, JTerm poTerm, InitConfig proofConfig)
     }
 
     @Override
-    public InfFlowProof createProofObject(String proofName, String proofHeader, JTerm poTerm,
+    public InfFlowProof createProofObject(String proofName,
+            KeyAst.@Nullable Declarations proofHeader, JTerm poTerm,
             InitConfig proofConfig) {
         final InfFlowProof proof = new InfFlowProof(proofName, poTerm, proofHeader, proofConfig);
 

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/InfFlowProof.java

@@ -7,6 +7,7 @@
 
 import de.uka.ilkd.key.informationflow.po.InfFlowProofSymbols;
 import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.proof.BuiltInRuleIndex;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.Statistics;
@@ -20,6 +21,8 @@
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * The proof object used by Information Flow Proofs.
  *
@@ -39,12 +42,14 @@ public class InfFlowProof extends Proof {
      */
     private SideProofStatistics sideProofStatistics = null;
 
-    public InfFlowProof(String name, Sequent sequent, String header, TacletIndex rules,
+    public InfFlowProof(String name, Sequent sequent, KeyAst.@Nullable Declarations header,
+            TacletIndex rules,
             BuiltInRuleIndex builtInRules, InitConfig initConfig) {
         super(name, sequent, header, rules, builtInRules, initConfig);
     }
 
-    public InfFlowProof(String name, JTerm problem, String header, InitConfig initConfig) {
+    public InfFlowProof(String name, JTerm problem, KeyAst.@Nullable Declarations header,
+            InitConfig initConfig) {
         super(name, problem, header, initConfig);
     }
 

key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java

@@ -1281,6 +1281,7 @@ private ProgramVariable getProgramVariableForFieldSpecification(
                 Type recoderType =
                     (getServiceConfiguration().getSourceInfo()).getType(recoderVarSpec);
                 final ClassType recContainingClassType = recoderVarSpec.getContainingClassType();
+
                 final ProgramElementName pen =
                     new ProgramElementName(makeAdmissibleName(recoderVarSpec.getName()),
                         makeAdmissibleName(recContainingClassType.getFullName()));

key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java

@@ -5,8 +5,8 @@
 
 
 import java.util.Collection;
-import java.util.HashMap;
 import java.util.Map;
+import java.util.TreeMap;
 
 import de.uka.ilkd.key.java.abstraction.*;
 import de.uka.ilkd.key.java.expression.Literal;
@@ -41,7 +41,7 @@ public final class TypeConverter {
     private final Services services;
 
     // Maps LDT names to LDT instances.
-    private final Map<Name, LDT> LDTs = new HashMap<>();
+    private final Map<Name, LDT> LDTs = new TreeMap<>();
 
     private HeapLDT heapLDT = null;
     // private IntegerLDT integerLDT = null;

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java

@@ -106,7 +106,10 @@ public void check(Services javaServ, KeYJavaType containingClass) throws Convert
         String qualifier =
             name.lastIndexOf('.') != -1 ? name.substring(0, name.lastIndexOf('.')) : "";
         name = name.substring(name.lastIndexOf('.') + 1);
-        TypeRef tr = new TypeRef(new ProgramElementName(name, qualifier), 0, null, containingClass);
+        final ProgramElementName programName =
+            qualifier.isEmpty() ? new ProgramElementName(name)
+                    : new ProgramElementName(name, qualifier);
+        TypeRef tr = new TypeRef(programName, 0, null, containingClass);
         ExecutionContext ec = new ExecutionContext(tr, null, null);
 
         for (int i = 0; i < actual; i++) {

key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java

@@ -151,7 +151,6 @@ public final SortDependingFunction getExactInstanceofSymbol(Sort sort, TermServi
     @Override
     public boolean isResponsible(Operator op, JTerm[] subs, Services services,
             ExecutionContext ec) {
-        assert false;
         return false;
     }
 

key.core/src/main/java/de/uka/ilkd/key/logic/ProgramElementName.java

@@ -70,6 +70,7 @@ public ProgramElementName(String name, NameCreationInfo creationInfo, Comment[]
 
     public ProgramElementName(String n, String q) {
         super(q + "::" + n);
+        // weigl: This check does not make sense
         assert !q.isEmpty() : "Tried to create qualified name with missing qualifier";
 
         this.qualifierString = q.intern();

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.nparser;
 
+import java.io.PrintWriter;
 import java.net.URI;
 import java.net.URISyntaxException;
 import java.net.URL;
@@ -170,20 +171,9 @@ public ProblemInformation getProblemInformation() {
          * declarations of sorts, program variables, schema variables, predicates, and more.
          * See the grammar (KeYParser.g4) for more possible elements.
          */
-        public String getProblemHeader() {
+        public KeyAst.@Nullable Declarations getProblemHeader() {
             final KeYParser.DeclsContext decls = ctx.decls();
-            if (decls != null && decls.getChildCount() > 0) {
-                final Token start = decls.start;
-                final Token stop = decls.stop;
-                if (start != null && stop != null) {
-                    int a = start.getStartIndex();
-                    int b = stop.getStopIndex();
-                    Interval interval = new Interval(a, b);
-                    CharStream input = ctx.start.getInputStream();
-                    return input.getText(interval);
-                }
-            }
-            return "";
+            return new KeyAst.Declarations(decls);
         }
     }
 
@@ -319,4 +309,136 @@ private static List<ScriptCommandAst> asAst(URI file,
             return new ScriptCommandAst(it.cmd.getText(), nargs, pargs, loc);
         }
     }
+
+    /// Represents the user declarations in a KeY file.
+    ///
+    /// @author weigl
+    public static class Declarations extends KeyAst<KeYParser.DeclsContext> {
+        protected Declarations(KeYParser.DeclsContext ctx) {
+            super(ctx);
+        }
+
+        public java.io.@Nullable File getJavaSourceLocation() {
+            try {
+                KeYParser.String_valueContext value =
+                    ctx.javaSource(0).oneJavaSource().string_value(0);
+                String v = ParsingFacade.getValueDocumentation(value);
+                return new java.io.File(v);
+            } catch (NullPointerException | IndexOutOfBoundsException e) {
+                {
+                    return null;
+                }
+            }
+        }
+
+        /// Prints the definitions, independent of paths, to the given {@link PrintWriter}.
+        public void printDefinitions(PrintWriter out) {
+            ctx.accept(new KeYParserBaseVisitor<@Nullable Object>() {
+                @Override
+                public @Nullable Object visitOne_include(KeYParser.One_includeContext ctx) {
+                    if (ctx.absfile != null) {
+                        out.printf("\\include %s;", ctx.absfile.getText());
+                    }
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitOptions_choice(KeYParser.Options_choiceContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitOption_decls(KeYParser.Option_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitSort_decls(KeYParser.Sort_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitProg_var_decls(KeYParser.Prog_var_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitSchema_var_decls(
+                        KeYParser.Schema_var_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitPred_decls(KeYParser.Pred_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitFunc_decls(KeYParser.Func_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitTransform_decls(KeYParser.Transform_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitDatatype_decls(KeYParser.Datatype_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+
+                @Override
+                public @Nullable Object visitRuleset_decls(KeYParser.Ruleset_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+
+                @Override
+                public @Nullable Object visitContracts(KeYParser.ContractsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitInvariants(KeYParser.InvariantsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                private void printAsIs(ParserRuleContext ctx) {
+                    if (ctx != null) {
+                        final Token start = ctx.start;
+                        final Token stop = ctx.stop;
+                        if (start != null && stop != null) {
+                            int a = start.getStartIndex();
+                            int b = stop.getStopIndex();
+                            Interval interval = new Interval(a, b);
+                            CharStream input = ctx.start.getInputStream();
+                            out.println(input.getText(interval));
+                        }
+                    }
+                }
+            });
+
+
+        }
+    }
 }