Proposed rule: loops must not be infinite (except when they must)

Detect the loops that might never terminate. Ignore loops that are infinite by design, e.g. an event-processing loop.

An idea of how to detect infinite loops: symbolically execute the loop and discover whether the early-exit statements in the loop body are reachable, and if not, whether the expression used in the termination condition remains the same after the iteration regardless of what happens during the iteration.

An idea of how to avoid FPs raised on loops intentionally made infinite: ignore loops with no termination condition, e.g. while(1), for( ; ; ).