[uhno]

For simple cases (such as the example in the GP comment) a compiler can easily infer those annotations. Complications are introduced in languages which allow aliasing. Precise alias analysis has been shown to be NP-hard [1] (as are many other compiler problems), and thus in general compilers must make very pessimistic assumptions to avoid making incorrect optimizations, such as allowing two functions to execute in parallel.

Other issues crop up due to the open-world assumption. This is especially true in the presence of separate compilation when trying to reason about global behavior. Example: does function f() in file f.c modify global variable g in file g.c? The compiler may not be able to prove that one way or another at compile-time (consider if file f.c was already compiled to object code f.o, and only g.c was being recompiled), and so it must assume that f() may modify g. This particular example can be solved with link-time optimization, but you get the idea of how complicated the real world can get.

[1] Horwitz, "Precise flow-insensitive may-alias analysis is NP-hard," TOPLAS 1997.