phanalist

E0036: Array Index Out of Bounds

E0036 reports array indexes that can be out of bounds. It is the array-index member of Phanalist’s bounded formal verification family (E0031-E0043). The family shares a Z3-backed engine that encodes path conditions and values, so a finding comes with a solver-backed counterexample rather than a heuristic guess.

What it checks

Negative and out-of-bounds array indexes
PHPDoc list<T> and non-empty-list<T> values, including count()/sizeof() lengths, appends, foreach keys, and isset() guards
First and last keys from array_key_first() and array_key_last() on tracked literal arrays, preserving PHP insertion order
Derived list lengths from array_merge() on list inputs and lengths preserved by array_map(), array_values(), and array_reverse()
Generic array<K,V> lengths, including lengths returned through PHPDoc contracts
Upper bounds from array_diff(), array_intersect(), array_unique(), array_filter(), and array_fill_keys(); exact lengths from array_keys(); count-derived lengths from array_fill(); padded lengths from array_pad(); PHP-compatible offset and length rules for array_slice(); and chunk counts from array_chunk()
The longest input length for multi-array array_map()
Guards in short-circuited && chains
Reachable symbolic indexes that can be out of bounds; indexes that cannot be modeled report unverified under unknown_policy: report
Literal accesses that are merely uncertain are not reported as hard out-of-bounds findings

Model limits

E0036 shares the model limits, loop bounds, and interprocedural behavior described in E0031. It does not assume arbitrary relationships between two lists, such as a key from one list being valid for another. It only uses the length relationships produced by the modeled built-ins and by explicit guards or assertions.

Configuration

rules:
  E0036:
    php_version: "8.4"
    check_array_index: true

See E0031 for the shared model limits, unknown_policy behavior, and per-code configuration.

This site is open source. Improve this page.