Sound (key word here) analysis of this form, which is known flow-sensitive, is remarkably slow. Soundness is required if you want "provable" rather than "99.9

Sound (key word here) analysis of this form, which is known flow-sensitive, is remarkably slow. Soundness is required if you want "provable" rather than "99.99%" correct. So much so that we have even had scalable context-sensitive interprocedural analysis for at least a decade longer than we have ever scalable flow-sensitive analysis in most contexts. For example, pointer analysis, which matters here, is ni that class. It is easy to find context sensitive flow-insensitive pointer analysis that scales very well, and has been easy for >1 decade. flow-sensitive -- still much harder in practice. A few papers here and there, but ... You can do halfway flow sensitive analysis with SSA and get it in a reasonable time bound but it's not the same for something like this. This is more of a problem than something like the standard library handling, because the standard library is a library and can be pre-computed into summaries, and the relevant summaries change very infrequently (IE to the original example, how much of the buffer read overwrites does not change every glibc release) Theses sorts of annotation based schemes are also not new - we've also had summary based algorithms that can do this sort of thing for decades. The algorithmic capabilities here have not really changed, and the improvement in computing power has not helped enough because lots of the sound algorithms are, worst case, cubic or exponential. In the end just remember if it was cheap, easy, and usable, it wouldn't be a problem, because it would already be done.