diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java index 2e98c55031f..fca25c71817 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java @@ -320,6 +320,7 @@ private ParseResult 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 readCompilationUnits( Path parent, Collection files, FileRepo repo) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java index 8b679cad60c..e1570ddff3e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java +++ b/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 c, ImmutableArray body, diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/Declaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/Declaration.java index b0ea7da810d..c654a821d81 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/Declaration.java +++ b/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 getModifiers(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/JavaNonTerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/JavaNonTerminalProgramElement.java index 23b1bc78c90..63094013252 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/JavaNonTerminalProgramElement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/JavaNonTerminalProgramElement.java @@ -57,6 +57,7 @@ public JavaNonTerminalProgramElement(PositionInfo pi, List 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 arr, ProgramElement el) { for (int i = 0, sz = arr.size(); i < sz; i++) { if (arr.get(i) == el) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java index 91470cdac79..a0d287d8cc6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java +++ b/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 { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/Throws.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/Throws.java index 5a0d8663ed1..47f3fcf3de3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/Throws.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/Throws.java @@ -20,6 +20,7 @@ * @author AutoDoc */ +@SuppressWarnings("deprecation") // exception list storage is bound to the deprecated ImmutableArray public class Throws extends JavaNonTerminalProgramElement implements TypeReferenceContainer { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/Operator.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/Operator.java index 2df8e812ba6..1f7643290b3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/Operator.java +++ b/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 children; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DLEmbeddedExpression.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DLEmbeddedExpression.java index d0e5d2a2103..201701fbd15 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DLEmbeddedExpression.java +++ b/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 comments, JFunction functionSymbol, @NonNull ImmutableArray children) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/ClashFreeSubst.java b/key.core/src/main/java/de/uka/ilkd/key/logic/ClashFreeSubst.java index 32efcda9fb7..b416c8736a4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/ClashFreeSubst.java +++ b/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 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[] newBoundVars = new ImmutableArray[arity]; for (int i = 0; i < arity; i++) { applyOnSubterm(t, i, newSubterms, newBoundVars); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java b/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java index 6c41dda6e4d..2b56ebf04fe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java +++ b/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 getPrefixElements(); /** returns the position of the first active child */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java index 6ca97351c1a..661743d8c36 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java +++ b/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 { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IObserverFunction.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IObserverFunction.java index bb961a22731..0521564c150 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IObserverFunction.java +++ b/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 getParamTypes(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramMethod.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramMethod.java index e41fe14edf9..22d82871032 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramMethod.java +++ b/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 getParameters(); // Methods from OberverFunction, TODO Create interface for ObersverFunction + @SuppressWarnings("deprecation") // contract of getParamTypes is bound to ImmutableArray ImmutableArray getParamTypes(); /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/JAbstractSortedOperator.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/JAbstractSortedOperator.java index 16eae2abc47..df2baf41f76 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/JAbstractSortedOperator.java +++ b/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 { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java index a28d4802325..c651fcf1edb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java @@ -227,7 +227,7 @@ private static ThreadLocal> 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[]> newNotSimplifiableCaches() { return ThreadLocal.withInitial(() -> { final LRU[] caches = (LRU[]) 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 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 apply(Goal goal, RuleApp ruleApp) { assert ruleApp instanceof OneStepSimplifierRuleApp diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java index adb10680cfd..15d4e768650 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java +++ b/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 boundVars, LogicVariable x, SVInstantiations insts) { @@ -946,6 +948,7 @@ public ImmutableList 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 findIfFormulaInstantiationsHelp( ImmutableList ruleSuccTail, ImmutableList ruleAntecTail, diff --git a/key.core/src/test/java/de/uka/ilkd/key/scripts/ProofScriptParserTest.java b/key.core/src/test/java/de/uka/ilkd/key/scripts/ProofScriptParserTest.java index 11ca805fed4..f7b5ae99a91 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/scripts/ProofScriptParserTest.java +++ b/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"; diff --git a/key.core/src/test/java/de/uka/ilkd/key/strategy/TieBreakComparatorPropertyTest.java b/key.core/src/test/java/de/uka/ilkd/key/strategy/TieBreakComparatorPropertyTest.java index a1d29e02140..adc80b5dcf2 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/strategy/TieBreakComparatorPropertyTest.java +++ b/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(); diff --git a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java index 4c96a788de7..e97fa955eab 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java +++ b/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<>(), diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java index 1dbdf1a50f3..9b33d320f42 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java +++ b/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 wrappedMap = new LinkedHashMapWrapper(tb.tt(), 1, TERM_LABELS_PROPERTY);