[kazinator]

Problem is, some undefined behaviors are actually correct. Some are documented extensions (a concept straight out of ISO C), and some are just nonportable situations that empirically work.

These could be handled in the prover; you just need an extended language definition. Or maybe not. Depending on what is being relied upon, it could be difficult.

In any case, a prover based on equating "correct" with "strictly conforming ISO C" is going to be of severely limited use. It might be good for some module-level assurance, like that some linked list or hash table module is perfect or whatever.

[Blaisorblade0]

But you are aware real-world compilers are exploiting more and more UB and keep breaking existing software? Maybe you are, but the comment does not seem to reflect that.

Either way: The good thing is, after compiler writers start exploiting a kind of UB they add options like `-fno-strict-aliasing` and pinky swear that option preserves the UB. I agree a useful checker should support real-world relevant C dialects.