How realistic is the "all function calls" part? Maybe I just don't see the bigger picture, but I would expect most function calls arguments to only be known at runtime, which of course makes static analysis not possible?
Obviously "all function calls" phrase cannot be absolute, but most can be caught with the analyzer giving one of proved/disproved/unknown result. The reason all cannot be caught is because pre/post are logical predicates on sets of values and are not part of the typing system.
To understand that, you have to know how a static analyzer works and specifically two of its functions, "Data Flow Analysis" and "Symbolic Execution".
It is Symbolic Execution that does static checking without the need for the actual runtime values to be known. It basically "executes" the code mathematically, building logical predicates over "sets of values" (indicated by the type of the variable) and thence trying to prove/disprove the formula using a solver. Note that the program is being "run" abstractly in the mathematical world using quantifiers just like you do in a mathematical proof.
If you know Hoare triples, and Dijkstra's WP-Calculus you know how to do this mechanically.
So the analyzer does two things; a) in the function itself it assumes pre is true and tries to prove post and b) at the call site it makes sure the paths leading up to the invocation satisfy the pre/post args/result needs thus chaining everything through the codebase. Both are done using symbolic execution. If it cannot prove/disprove the assertions, it remains silent (i.e. "unknown" result above) and leaves it to runtime checks to catch the violations.
Some resources:
1) How Static Analysis works - https://pvs-studio.com/en/blog/posts/1048/
2) A Gentle Introduction to Symbolic Execution for Software Security - https://can-ozkan.medium.com/a-gentle-introduction-to-symbol...
3) Scaling Symbolic Execution to Large Software Systems - https://arxiv.org/abs/2408.01909
See also: Catching Bugs Early: Validating C++ Contracts with Static Analysis - https://news.ycombinator.com/item?id=50379283