It's certainly less complete, but it's a little harder to decide what you want to prove statically.
If a function must-overflow the optimizer (hopefully) replaces the entire thing with an abort under ubsan, so you could look for that. But that's probably not sensitive enough.
And if the function is just 'x + 1' that may-overflow, but it's not important.
If a function must-overflow the optimizer (hopefully) replaces the entire thing with an abort under ubsan, so you could look for that. But that's probably not sensitive enough.
And if the function is just 'x + 1' that may-overflow, but it's not important.
Maybe you want this: http://pdos.csail.mit.edu/papers/stack:sosp13.pdf