On Mon, 27 Oct 2025 at 20:39, Charles-henri Gros via SG21
<sg21_at_[hidden]> wrote:
>
> As a developer of static analysis, I can state the following:
>
> I'm not trying to prove anything, however nice that would be. Proving almost anything in the presence of pointers or loops is largely impossible (see Rice's theorem).

I have static analysis tools that prove absence (or presence) of UB.
With limitations, and with configurable effort spent. The static
analysis tools
that my company sells don't seem to do that, but the tools of at least
two competitors (and, in various areas, partners and suppliers) do.

I want them to do more of that.