phanalist

E0040: Return Contract Violation

E0040 reports return values that contradict a declared return contract. It is the return-contract 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

• Native return types and PHPDoc @return contracts
• Missing return values on paths that must return a value
• never contracts that make following code unreachable
• Strict and weak PHP return coercion rules
• Numeric, string, list, non-empty, and shaped array contracts
• Generator returns are not checked against the generator return type

Model limits

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

Configuration

rules:
  E0040:
    php_version: "8.4"
    check_return_contracts: true

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

This site is open source. Improve this page.