Repository navigation
[TS] Constrain Array.indexOf to the first matching element #434
Description
Resolution (2026-10-14)
Audited against usvm main at 19866c959d.
The bounded Array.indexOf source model checks elements using strict equality, fromIndex and first-match ordering instead of returning an unconstrained index. Implementation: usvm #443.
Validation: All 41 TsSequenceEtsIrModelTest regressions passed, including indexOf equality and offset cases.
Original report and acceptance context, retained for traceability
Problem
The Array.indexOf approximation returns any in-range index or -1 without checking array contents.
Minimal TypeScript example
export function index(): number {
return [4, 7, 4].indexOf(4);
}Expected behavior
index() returns 0, never 1, 2 or -1. Model strict equality, fromIndex and first-match semantics in the supported array domain.
Current source evidence
Checked against USVM main 53dce8f3bca2713642c783ba8308a6a360a9e516. This exact snippet is a proposed regression from source audit; it has not yet been run as a new end-to-end test. #368 audits the existing call approximations but does not implement these individual fixes.
Acceptance criteria
- A focused test checks the symbolic outcome without reporting an approximation as exact semantics.
- The supported case agrees with concrete TypeScript/Node.js replay.
- Unsupported operand or environment cases remain explicit.
Activity