phanalist

E0033: intdiv() by Zero

E0033 reports intdiv() calls whose divisor can be zero. It is the intdiv()-by-zero 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

• intdiv($value, 0) and intdiv($value, $divisor) where $divisor can be zero
• Symbolic divisors, tracked array elements, and bounded integer ranges
• Guarded calls, including if, switch, match, short-circuit &&, and try/catch/finally paths
• Constant-return, identity, and PHPDoc method/function summaries

Model limits

E0033 shares the model limits, loop bounds, and interprocedural behavior described in E0031.

Configuration

rules:
  E0033:
    php_version: "8.4"
    check_intdiv: true

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

This site is open source. Improve this page.