phanalist

E0032: Modulo by Zero

E0032 reports modulo whose right operand can be zero. It is the modulo 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

• % and %= where the divisor can be zero
• Literal zero, symbolic zero, and zero reached through tracked arrays or expressions
• Guarded modulo, including if, switch, match, short-circuit &&, and try/catch/finally paths
• Loop exit values merged with the feasible zero-iteration path
• Constant-return, identity, and PHPDoc method/function summaries

Model limits

E0032 shares the model limits, loop bounds, and interprocedural behavior described in E0031. A clean result is relative to that model, not a proof of every possible PHP execution.

Configuration

Each verification code has its own settings block. The relevant check is:

rules:
  E0032:
    php_version: "8.4"
    check_modulo: true

check_modulo controls the modulo-by-zero check for E0032. Other checks are configured under their own codes.

This site is open source. Improve this page.