Skip to content

[JVM] Make the pinned model string length bound configurable - #631

Closed
CaelmBleidd wants to merge 1 commit into
caelmbleidd/jvm-residual-call-policiesfrom
caelmbleidd/jvm-model-string-domain-review
Closed

CaelmBleidd wants to merge 1 commit into
caelmbleidd/jvm-residual-call-policiesfrom
caelmbleidd/jvm-model-string-domain-review

Conversation

@CaelmBleidd

Copy link
Copy Markdown
Member

Expose the pinned stdlib model length <= 50 restriction as an explicit option. The default preserves it; disabling the bound skips only the known private String._assumeInvariants assumeSymbolic call, retaining ordinary user assumptions and the other string invariants. The version-specific helper contract is documented in the implementation.

Validation: 4 regressions cover the legacy bound, length 51, user assumptions and a character beyond the boundary. Combined descendant 2ac27c1ae: all 12 focused tests passed and JVM Detekt main/test completed under the exclusive local build lock. Standalone PR-head CI is separate.

Stack: targets caelmbleidd/jvm-residual-call-policies; review only this layer, merge/rebase its prerequisite first, and recheck the final main integration. Existing JVM fixes #562, #563 and #598 remain separate entries in the Calls wrap-up map. Frozen experiment artifacts are unchanged.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant