[nanolith]

The compiler really doesn't have the opportunity to simulate every possibility of code. It's not just the matter of whether the function is safe, but every possible use of the function, which the compiler may not see when it is focused on a single compilation unit or a library.

If you want this level of safety, which is possible in C, then you need to use a model checker. Model checking C isn't as trivial as adding a flag to the compiler, but it can be done with about as much overhead as unit testing, if a reasonable idiomatic style is followed, and if the model checker is used well.

It is still a decision problem, and thus has similar limitations, but you can perform steps to ensure that you have some level of soundness with unwinding assertions and other techniques.

[jmkr]

Thanks that's helpful I'll take a look at model checking.