[pjc50]

There is no "safe subset" of C. MISRA is fairly close, but all sorts of things that you might need, like integer arithmetic, have potential UB in C.

(The best current effort is https://sel4.systems/ , which is written in C but has a large proof of safety attached. The language design question is basically: should the proof be part of the language?)

[regularfry]

Given that undefined behaviour just means "undefined by the standard", do you get usefully closer to being able to identify a safe subset with the (MISRA/alternative, specific compiler, specific architecture) triple?

[pjc50]

No, undefined behavior does not mean "not defined by the standard", it means those places where the standard says "undefined behavior". And then the long and complicated war over "the compiler may assume that UB does not happen and then optimize on that basis".

You might be able to tighten it up in some specific cases, and those battles are being fought elsewhere, but there's stuff like lock lifetimes which you cannot do without substantial extra annotations inside or outside the language.

[regularfry]

Sorry, yes - poor wording on my part.

[PhilipRoman]

I found frama-c to be pretty good, including all the integer quirks