Static analysis has not proven to be especially helpful in finding bugs in SQLite. Static analysis has found a few bugs in SQLite, but those are the exceptions. More bugs have been introduced into SQLite while trying to get it to compile without warnings than have been found by static analysis.
This speaks more to the maturity and robustness of the SQLite codebase than it does of static analysis as a type of tool.
Static Analysis is very useful in the development phase of a project where you can treat them effectively as compiler warnings if your build system is setup that way.
...and that isn't to say that its not worth still using SA on mature codebases, just because a codebase is mature does not indicate its quality.
SA will capture issues related to the implementation but in itself it has no knowledge of application-specific behaviour.
Tests on the other hand do have application-specific knowledge and this is where their value lies.
Also, having these tools, but no coding rules by code contributors, enforced with real code-reviews and reviewer(s), will also deliver 'not worth it' results. Its a process, not a chisel.
Sure, it's better to catch them up front. But catching them later is still extremely valuable.
Fuzzing found real actionable bugs in SQLite. As I consider fuzzing a variant of static checking (it executes a subset of symbolic evaluation space), I consider the result above as a resounding success of static methods.
Also please look at the date when the phrase was added: https://web.archive.org/web/20090205181900/http://sqlite.org... - it's 2009, the very first version of the page! And they didn't change it a bit since.
Basically you base your damnation on an outdated information.
You cannot "examine the code" without executing it, partially or in full, with some input or intermediate values or (symbolically) with all of them.
I am sure I sound contrary to "common definitions" - so be it. I also think that dynamic typing is a subset of static typing, more or less for the same reason.
It is entirely possible to break a stream of text down into symbols and examine the relationship of those symbols without evaluating (i.e. executing) them. It is not really necessary or possible to know their meaning/definition at all, only their "shape" or the "part of speech" that they represent.
In the simplest form, static analyzers are a set of heuristic pattern matchers that a stream of text is sent through. It might get fancy and build an AST first, but that still does not constitute execution or evaluation in the technical sense.
You can prove that sqlite_exec("create table a ...insert into a ...select * from a where ...") is equal to, say list ["gaga", "gugu"], given supercompiler that is powerful enough. The paper above proves properties up to termination of programs, so it will prove (Haskell) sum [1..] == sum (map (+1) [0..]) as equal (up to computation of the lists).
Would you consider this an example of static analysis?
If answer is "yes", bear in mind that supercompilation includes evaluation of the programs - basically, supercompiler executes them, looking for states it already seen.
I also would like to hear reasons why if answer is "no".
It's pretty simple: if you execute the program code, whether directly on a processor or in an virtual processor/emulator, it's dynamic analysis. Otherwise it's a variant of static analysis.
Note also:
> We want verification to be about proving absence of bugs, not about finding bugs
A more interesting comparison would be between the most powerful/restrictive static analyses vs. the most powerful dynamic analyses.
Every release of FreeRADIUS (http://freeradius.org) gets run through three different static analysis tools. They each find slightly different things.
At this point, the bulk of issues they find are false positives. Addressing those doesn't create bugs, and I'm not sure why it would.
We found Coverity to be prohibitively expensive; but unfortunately there isn't any real alternative!
Anything that changes behaviour could create bugs. Here is an example
signed bar = something_possibly_negative();
if(some_case) {
bar = calc_returning_unsigned_where_MSB_is_an_error_flag();
if(bar < 0)
return ERROR;
}
// now bar is valid, whether negative or positive.
long long bar = something_possibly_negative();
For more in this vein see: http://ithare.com/best-practices-vs-witch-hunts/