phanalist

E0035: Missing Array Key

E0035 reports reads of keys that are missing from tracked literal arrays. It is the array-key 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

• Missing string and integer keys in tracked literal arrays
• Keys returned by array_key_first() and array_key_last() for tracked literal arrays, preserving PHP insertion order
• Nested literal array shapes
• Reads guarded by isset() and ??
• Arrays forgotten after writes through untracked paths or by-reference calls
• Keys checked through bounded branches and short-circuit conditions

Model limits

E0035 shares the model limits, loop bounds, and interprocedural behavior described in E0031. It reports missing keys, not list bounds; use E0036 for out-of-bounds list indexes.

Configuration

rules:
  E0035:
    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.