Pass 2: Suppress deprecation warnings in key.core (ImmutableArray-bound APIs)

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

@@ -320,6 +320,7 @@ private ParseResult<CompilationUnit> parseCompilationUnit(Path filename,
      * @param repo the repo to use for reading
      * @return a list of KeY structured compilation units.
      */
+    @SuppressWarnings("deprecation") // JavaLogger.print is deprecated; used for AST diagnostics
     public List<de.uka.ilkd.key.java.ast.CompilationUnit> readCompilationUnits(
             Path parent,
             Collection<Path> files, FileRepo repo)

key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java

@@ -51,6 +51,7 @@ public ContextStatementBlock(Statement[] body, IExecutionContext executionContex
         this.executionContext = executionContext;
     }
 
+    @SuppressWarnings("deprecation") // ctor delegates StatementBlock body, bound to ImmutableArray
     public ContextStatementBlock(
             PositionInfo pi, List<Comment> c,
             ImmutableArray<? extends Statement> body,

key.core/src/main/java/de/uka/ilkd/key/java/ast/Declaration.java

@@ -19,5 +19,6 @@ public interface Declaration extends NonTerminalProgramElement {
      *
      * @return the (original) list of modifiers wrapped .
      */
+    @SuppressWarnings("deprecation") // contract of getModifiers is bound to ImmutableArray
     ImmutableArray<Modifier> getModifiers();
 }

key.core/src/main/java/de/uka/ilkd/key/java/ast/JavaNonTerminalProgramElement.java

@@ -57,6 +57,7 @@ public JavaNonTerminalProgramElement(PositionInfo pi, List<Comment> comments) {
      *        the element to look for
      * @return the index of the element (-1 if not found)
      */
+    @SuppressWarnings("deprecation") // helper operates on the deprecated ImmutableArray
     protected int getArrayPos(ImmutableArray<ProgramElement> arr, ProgramElement el) {
         for (int i = 0, sz = arr.size(); i < sz; i++) {
             if (arr.get(i) == el) {

key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java

@@ -30,6 +30,8 @@
 /**
  * Statement block. taken from COMPOST and changed to achieve an immutable structure
  */
+@SuppressWarnings("deprecation") // statement body/prefix API is bound to the deprecated
+                                 // ImmutableArray
 public class StatementBlock extends JavaStatement implements StatementContainer,
         TypeDeclarationContainer, VariableScope, TypeScope, ProgramPrefix {
 

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/Throws.java

@@ -20,6 +20,7 @@
  * @author <TT>AutoDoc</TT>
  */
 
+@SuppressWarnings("deprecation") // exception list storage is bound to the deprecated ImmutableArray
 public class Throws extends JavaNonTerminalProgramElement implements TypeReferenceContainer {
 
 

key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/Operator.java

@@ -20,6 +20,8 @@
  * @author AL
  */
 
+@SuppressWarnings("deprecation") // AST children storage is bound to the deprecated ImmutableArray
+                                 // API
 public abstract class Operator extends JavaNonTerminalProgramElement
         implements Expression, ExpressionContainer {
     protected final ImmutableArray<Expression> children;

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

@@ -32,6 +32,7 @@
 public class DLEmbeddedExpression extends Operator {
     private final JFunction functionSymbol;
 
+    @SuppressWarnings("deprecation") // ctor parameter bound to the deprecated ImmutableArray
     public DLEmbeddedExpression(
             PositionInfo pi, List<Comment> comments, JFunction functionSymbol,
             @NonNull ImmutableArray<Expression> children) {

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

@@ -13,6 +13,8 @@
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableSet;
 
+@SuppressWarnings("deprecation") // clash-free substitution API is bound to the deprecated
+                                 // ImmutableArray
 public class ClashFreeSubst {
     protected final QuantifiableVariable v;
     protected final JTerm s;
@@ -86,7 +88,8 @@ protected static ImmutableArray<QuantifiableVariable> getSingleArray(
     private JTerm applyOnSubterms(JTerm t) {
         final int arity = t.arity();
         final JTerm[] newSubterms = new JTerm[arity];
-        @SuppressWarnings("unchecked")
+        @SuppressWarnings({ "unchecked", "rawtypes" }) // raw new ImmutableArray[...] array +
+                                                       // unchecked cast
         final ImmutableArray<QuantifiableVariable>[] newBoundVars = new ImmutableArray[arity];
         for (int i = 0; i < arity; i++) {
             applyOnSubterm(t, i, newSubterms, newBoundVars);

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

@@ -30,6 +30,7 @@ public interface ProgramPrefix extends NonTerminalProgramElement {
     /**
      * returns an array with all prefix elements starting at this element
      */
+    @SuppressWarnings("deprecation") // contract of getPrefixElements is bound to ImmutableArray
     ImmutableArray<ProgramPrefix> getPrefixElements();
 
     /** returns the position of the first active child */

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

@@ -26,6 +26,7 @@
  * This class is used to encapsulate knowledge about the internal term structures. See
  * {@link TermBuilder} for more convenient methods to create terms.
  */
+@SuppressWarnings("deprecation") // term-creation API is bound to the deprecated ImmutableArray
 public final class TermFactory {
 
 

key.core/src/main/java/de/uka/ilkd/key/logic/op/IObserverFunction.java

@@ -56,6 +56,7 @@ public interface IObserverFunction extends SortedOperator, Operator {
      * Returns the parameter types of this observer symbol. "Parameters" here includes only the
      * *explicit* parameters, not the heap and the receiver object.
      */
+    @SuppressWarnings("deprecation") // contract of getParamTypes is bound to ImmutableArray
     ImmutableArray<KeYJavaType> getParamTypes();
 
 }

key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramMethod.java

@@ -74,9 +74,11 @@ public interface IProgramMethod
 
     int getParameterDeclarationCount();
 
+    @SuppressWarnings("deprecation") // contract of getParameters is bound to ImmutableArray
     ImmutableArray<ParameterDeclaration> getParameters();
 
     // Methods from OberverFunction, TODO Create interface for ObersverFunction
+    @SuppressWarnings("deprecation") // contract of getParamTypes is bound to ImmutableArray
     ImmutableArray<KeYJavaType> getParamTypes();
 
     /**

key.core/src/main/java/de/uka/ilkd/key/logic/op/JAbstractSortedOperator.java

@@ -20,6 +20,8 @@
 /**
  * Abstract sorted operator class offering some common functionality.
  */
+@SuppressWarnings("deprecation") // constructor signatures are bound to the deprecated
+                                 // ImmutableArray
 public abstract class JAbstractSortedOperator extends AbstractSortedOperator
         implements Sorted, Operator {
 

key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java

@@ -227,7 +227,7 @@ private static ThreadLocal<LRU<SequentFormula, Boolean>> newApplicabilityCache()
     }
 
     /** A fresh, empty per-worker not-simplifiable cache (one {@link LRU} map per rule set). */
-    @SuppressWarnings("unchecked")
+    @SuppressWarnings({ "unchecked", "rawtypes" }) // raw LRU[] array creation + unchecked cast
     private static ThreadLocal<LRU<JTerm, JTerm>[]> newNotSimplifiableCaches() {
         return ThreadLocal.withInitial(() -> {
             final LRU<JTerm, JTerm>[] caches = (LRU<JTerm, JTerm>[]) new LRU[ruleSets.size()];
@@ -397,6 +397,7 @@ private SequentFormula simplifyPosOrSub(Goal goal,
      *
      * @param protocol
      */
+    @SuppressWarnings("deprecation") // TermLabelManager.instantiateLabels returns ImmutableArray
     private JTerm replaceKnownHelper(
             Map<TermReplacementKey, PosInOccurrence> map, JTerm in,
             boolean inAntecedent,
@@ -667,6 +668,7 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) {
     }
 
     @Override
+    @SuppressWarnings("unchecked") // assumesInsts() returns a raw ImmutableList
     public @NonNull ImmutableList<Goal> apply(Goal goal, RuleApp ruleApp) {
 
         assert ruleApp instanceof OneStepSimplifierRuleApp

key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java

@@ -267,6 +267,8 @@ private static JTerm getTermBelowQuantifier(org.key_project.prover.rules.Taclet
      *        SchemaVariables
      * @return true iff the instantiation of a Bound Schemavariable contains the given Logicvariable
      */
+    @SuppressWarnings("deprecation") // bound-schema-variable matching uses deprecated
+                                     // ImmutableArray
     private static boolean contains(ImmutableArray<QuantifiableVariable> boundVars,
             LogicVariable x,
             SVInstantiations insts) {
@@ -946,6 +948,7 @@ public ImmutableList<TacletApp> findIfFormulaInstantiations(Sequent seq, Service
      *        program model
      * @return a list of tacletapps with the found if formula instantiations
      */
+    @SuppressWarnings("deprecation") // assume-formula instantiations are ImmutableArray-based
     private ImmutableList<TacletApp> findIfFormulaInstantiationsHelp(
             ImmutableList<SequentFormula> ruleSuccTail,
             ImmutableList<SequentFormula> ruleAntecTail,

key.core/src/test/java/de/uka/ilkd/key/scripts/ProofScriptParserTest.java

@@ -72,6 +72,7 @@ void higherOrder() {
      * not keep the stray '\r' inside the argument value.
      */
     @Test
+    @SuppressWarnings("deprecation") // test deliberately exercises the legacy ScriptLineParser
     void scriptLineParserIgnoresCarriageReturns() throws Exception {
         String crlf = "select formula=\"line one\r\nline two\";\r\n";
 

key.core/src/test/java/de/uka/ilkd/key/strategy/TieBreakComparatorPropertyTest.java

@@ -181,6 +181,7 @@ void formulaComparatorAgreesWithTheWalk() {
      * not equal.
      */
     @Test
+    @SuppressWarnings("deprecation") // labels are passed via the deprecated ImmutableArray
     void orderingHashesIgnoreLabels() {
         final var services = de.uka.ilkd.key.rule.TacletForTests.services();
         final TermFactory tf = services.getTermFactory();

key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java

@@ -109,6 +109,7 @@ public TestTriggersSet() {
     }
 
     @BeforeEach
+    @SuppressWarnings("deprecation") // Proof.add and NamespaceSet ctor are deprecated
     public void setUp() {
         // sort
         r = new SortImpl(new Name("r"));
@@ -217,6 +218,7 @@ public void setUp() {
 
     }
 
+    @SuppressWarnings("deprecation") // NamespaceSet ctor is deprecated
     private JTerm parseTerm(String termstr) {
         return TacletForTests.parseTerm(termstr,
             new NamespaceSet(variables, functions, sorts, new Namespace<>(), new Namespace<>(),

key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java

@@ -275,6 +275,7 @@ public void testRenamingTermProperty() {
     }
 
     @Test
+    @SuppressWarnings("deprecation") // ctor variant takes deprecated ImmutableArray args
     public void testConstructors() {
         LinkedHashMapWrapper<JTerm, Integer> wrappedMap =
             new LinkedHashMapWrapper<JTerm, Integer>(tb.tt(), 1, TERM_LABELS_PROPERTY);