That would be an immense undertaking. It’s not really just that some statement or expression is unreachable (we have __builtin_unreachable() in GCC for stuff like that) but that certain states are unreachable.
For example,
int buffer_len(struct buffer *buf) {
return buf->end - buf->start;
}
There are at least three states that trigger undefined behavior: buf is not a valid pointer, buf->end - buf->start doesn’t fit in int, and buf->end and buf->start don't point to the same object.
I’m not sure how you would annotate this. At the function call site, you would somehow need to show that buf is a valid pointer, and that start/end point to same object and the difference fits in an int. It would start looking more like Coq or Agda than C.
Honestly, I think if you really want this kind of safety, your options are to use formal methods or switch to a different language.
There’s also this weird assumption here that the compiler detects undefined behavior in your program and then mangles it. It’s really the opposite—the compiler assumes that there is no undefined behavior in your program, and optimizes accordingly. In practice you can turn optimizations off and get something much closer to the “machine model” of C (which doesn’t really exist anyway) but most people hate it because their code is too slow.