https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109914

--- Comment #9 from Paul Eggert <eggert at cs dot ucla.edu> ---
(In reply to Jan Hubicka from comment #7)
> The idea is to help developers to annotate i.e. binary tree search function,
> which he clearly knows is always to be finite, but compiler can not prove it.

There's no need for GCC to prove it as GCC can assume it, at least for typical
cases such as the attached test case. ISO C23 § 6.8.6.1 ¶ 4 says:

An iteration statement may be assumed by the implementation to terminate if its
controlling expression is not a constant expression and none of the following
operations are performed in its body, controlling expression or (in the case of
a for statement) its expression-3:

  — input/output operations
  — accessing a volatile object
  — synchronization or atomic operations.

Reply via email to