Frama-C — Framework for Static Analysis of the C language
C source code → Abstract Syntax Tree
Annotate syntax trees with static analysis.