Static code analysis is extremely difficult. You have to have a notion of what an "error" is, and the complexity of interaction between different pieces of a codebase grows exponentially, making feasible analysis of big projects very difficult without throwing in heuristics to simplify the analysis at a cost of loss of precision.

Well, unfortunately most interesting static analysis problems are undecidable. There can be no "general" solution.

What we have in practice are approximations and heuristics; over time we will develop better approximations for the kinds of code people write in practice. Unfortunately fragility of analysis will always be a problem; if you change your code just a little bit then reasoning may fail.

As someone who has spent years doing research on shape analysis my personal belief is that the dream of a fully automated "find my bugs" static analysis is unrealistic. Some of the problems you must solve to analyze the heap, say, are very hard indeed.

We need to think more about the interactions between language design and verification, rather than hoping that people will build better tools to analyze existing code. Strong typing (e.g., the Hindley-Milner type system) is one example of a sweet spot that demonstrates how language design (type annotation, type declarations) interacts with tools (type inference, type checking). Type systems are some of the most widely used bug finding tools today. Trying to build verification tools without considering language design is always going to be difficult.