Static analysis tools for C suffer from modularity issues: These tools are primarily based on abstract interpretation, so their results are very sensible to the

Static analysis tools for C suffer from modularity issues: These tools are primarily based on abstract interpretation, so their results are very sensible to the control flow of your program. This means that your procedures, as analyzed by these tools, are connected by monstrous preconditions and invariants that describe the state of your program in each control flow path the program could possibly take. For obvious reasons, this doesn't scale.