Now I'm really curious to see some non-trivial C++ code that can be proved UB-free, but I understand you might not be at liberty to share.
________________________________
From: Ville Voutilainen <ville.voutilainen_at_[hidden]>
Sent: Monday, October 27, 2025 11:50 AM
To: sg21_at_[hidden] <sg21_at_[hidden]>
Cc: sg15_at_[hidden] <sg15_at_[hidden]>; Charles-henri Gros <chgros_at_[hidden]>
Subject: Re: [isocpp-sg21] [isocpp-sg15] P3835 -- Different contract checking for different libraries

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.