Repository navigation
Conversation
wadoon
changed the base branch from
weigl/cleanwarnings
to
weigl/cw-unchecked-rawtypes
October 24, 2026 22:26
wadoon
force-pushed
the
weigl/cw-unchecked-rawtypes
branch
from
October 24, 2026 22:31
12b48da to
9ac3cb2
Compare
Suppress deprecated APIs where they are bound to external library contracts (URL/URLStreamHandler constructors, recoder's getMembers()/getParamTypes() returning ImmutableArray); no behavior changes. Co-Authored-By: OpenCode (KIT Medium)
ImmutableArray is baked into the public term API (TermImpl, TermFactory, recoder); migration is not local, so annotate the bound methods and classes. Co-Authored-By: OpenCode (KIT Medium)
…core.matcher ImmutableArray is part of the public instantiation/cache APIs; the AssumesFormulaInstantiationCache union array requires a raw Pair array (generic array creation is not possible). Co-Authored-By: OpenCode (KIT Medium)
…e.testgen Migrate the genuinely local sites (ImmutableArray->ImmutableList in BasicBlockExecutionSnippet, raw Assignment->Assignment<?> in BasicSymbolicExecutionSnippet); suppress settings overrides the Settings interface still requires. Co-Authored-By: OpenCode (KIT Medium)
ImmutableArray dominates the term/label APIs (JTerm, TermBuilder, TermLabelManager, JavaInfo, SVInstantiations); all occurrences are bound to deprecated library contracts, so they are suppressed at the narrowest scope with explanatory comments. Unchecked casts in SVInstantiations are inherent to the map-backed instantiation store. Co-Authored-By: OpenCode (KIT Medium)
GeneralFailureEvent stays in use to preserve UI notification behavior; the Properties-based readSettings/writeSettings overloads remain because the Settings interface requires them. Co-Authored-By: OpenCode (KIT Medium)
wadoon
force-pushed
the
weigl/cw-unchecked-rawtypes
branch
from
October 25, 2026 00:57
9ac3cb2 to
5c28dc3
Compare
wadoon
force-pushed
the
weigl/cw-deprecation-main
branch
from
October 25, 2026 00:57
541e17d to
7299256
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Fix
[deprecation](plus[rawtypes]/[unchecked]) javac lint warnings in 31main-source files of
key.util,key.ncore,key.ncore.calculus,key.ncore.matcher,key.core,key.core.infflow,key.core.testgen,key.ui,keyext.isabelletranslation. 6 commits, one per module group.Numbers
150 occurrences handled:
ImmutableArray→ImmutableListinBasicBlockExecutionSnippet; rawAssignment→Assignment<?>inBasicSymbolicExecutionSnippet.0 targeted warnings remain in the 31 files (verified on a clean compile).
Reasoning highlights
ImmutableArray, whose contract is boundend-to-end through
Term/TermBuilder/operator APIs — migrating singlecall sites would change cross-type
equals/subs()semantics (e.g.TermLabelManager.replaceTermcomparesnewSubs.equals(term.subs())), sosuppression with justification is the behavior-preserving choice.
Full removal is the topic of Remove deprecated ImmutableArray in favor of ImmutableList #4001 (whose branch this stack is based on).
TermBuilderdeprecations not in theincremental baseline inventory; all were fixed within the same 31-file scope.
History audit (serial/this-escape)
Audited for the campaign cleanup: this branch contains NO serial or this-escape
fixes (no serialVersionUID, transient or serial/this-escape suppressions
anywhere in its 6 commits) — nothing to remove; history unchanged, head
541e17d.
Draft — part of the warning-cleanup stack on
weigl/cleanwarnings(→ PR #4001). No logic, signature or behavior changes.
Commits carry
Co-Authored-By: OpenCode (KIT Medium).Linear-stack head:
729925645e(re-based on the rebuilt #4004).