| |
The Leading Commercial Tools
- CodeSonar (Grammatech)
A new member of the CodeSurfer family (see below). The
tool is very effective in spotting code defects, and suspicious code fragments.
The tool is currently being extended with a rule checker for set of
coding rules for safety critical code, which will
make it extra attractive for high integrity applications. Especially good at
intra-procedural analysis. Highly recommended.
- Coverity
Leading edge tool based on Dawson Engler's
methodology for
source code analysis of large code bases. An extended version
of the tool supports user-defined properties in the Metal language.
Very few false positives, but can be expensive.
- KlocWork
Support for static error detection, with added project management
and project visualization capabilities. Fast, almost as thorough as
Coverity, and not quite as expensive. Especially good at finding array bound violations.
A capability for user-defined checks is pending.
- PolySpace
Marketed by a French company co-founded by students of
Patrick Cousot
(pioneer in the area of abstract interpretation).
Polyspace claims it can intercept 100% of the runtime errors in C programs.
(See
cverifier.htm.)
Customers are in the airline industry and the European space program.
Can be thorough, but also very slow, and does not scale beyond
a few thousand lines of code. Does not support full ANSI-C language
(e.g., it places restrictions on the use of gotos).
- Purify (Rational)
This tool is focused primarily on the detection of memory leaks, and not on
general source code analysis. It is used fairly broadly.
- The Lint family, e.g.
PC-Lint/FlexeLint (Gimpel),
Lint Plus (Cleanscape)
Generic source code analysis, value tracking, some types of array indexing errors.
Suffers from high, sometimes very high, false positive rates, but the
output can be customized with flags and code annotations.
-
PREfix and PREfast (Microsoft)
Effective, but Microsoft proprietary, tools.
PREfix was developed by Jon Pincus;
MicroSoft acquired the tool when it bought Pincus' company.
PREfast is a lighter weight tool, developed within Microsoft
as a faster alternative to PREfix (though it is not based on PREfix
itself). Both these tools are reported to be
very effective in intercepting defects early, and come with
filtering methods for the output to reduce the false positive ratio.
PREfast allows for new defect patterns to be defined via plugins.
Less than 10% of the code of PREfix is said to concern with analysis
per se, most applies to the filtering and presentation of output, to
reduce the number of false positives.
- Safer C (Oakwood Computing)
Based on L. Halton's 1995 book on Safer C, now out of print,
covering code analysis and enforcement of coding guidelines. Not found to be too
useful in our tests.
Academic and Research tools
- Calysto
(new) a tool by Domagoj Babic
- Saturn
(new) by Alex Aiken and others at Stanford.
- mygcc (new)
An extension of the gcc compiler supporting user-defined
checks written in a simple formalism, that can be checked efficiently.
Path queries can be run on the control-flow graph of
functions, specifying a start node, a stop node, and constraints on the
path in between.
Sample queries are provided that match many of the ones used in Engler's
early study using the Metal language (now supported by the Coverity tool).
A very interesting project that will hopefully find its
way into the main gcc distribution soon.
- ESC (Compaq/HP)
Extended static checker for Java and for Modula3.
developed by
Greg Nelson and colleagues, which
is based on a mix of theorem proving and static analysis.
It's thorough and effective, but also slow, and needs considerable knowledge
to run. This tool does not target C, and therefore does not properly
belong in this listing,
but we include it as one of the landmark research tools in this domain.
- LC-Lint
The descendent of the early research Unix version of lint, which was
written by Steve Johnson in 1979. This tool needs lots of annotations to work well,
and often produces overwhelming amounts of output.
- Vault (MicroSoft)
An experimental system, in development at MicroSoft by
Rob DeLine
and Manuel Fahndrich.
It is based on formal annotations
placed in the code.
- Astree (CNRS, France)
Astree is a static program analyzer for structured C programs,
but without support for dynamic memory allocation and recursion
(as used, for instance for embedded systems and in safety
critical systems).
The tool name is an acronym for Analyseur statique de
logiciels temps-reel embarques (static analyzer for
real-time embedded software). Among those working on
this tool are Patrick and Radhia Cousot.
- CGS (C Global Surveyor, NASA ARC)
An experimental tool at NASA Ames Research Center from
Guillaume Brat and
Arnaud Venet,
based on abstract interpretation techniques, inspired by Patrick Cousot.
Work in progress.
- C-Kit (Bell Labs).
A research toolkit developed at Bell Labs, with algorithms for pointer alias analysis,
program slicing,
etc. for ANSI C. Written in SML. Can produce parsetree and symbol table information,
but, as yet, not call flow graphs or function call graphs.
The principal researchers involved in this work
(Nevin Heintze,
Jon Riecke, Dave MacQueen)
are no longer at Bell Labs and development has stopped.
-
Uno (Bell Labs)
Lightweight tool for static analysis.
The tool is targeted at a small set of common programming
defects (Uninitialized data, Nil-pointer dereferencing, and
Out-of-bound array indexing, with the three initial letters giving
the tool its name). It also handles a range of simple, user-defined properties.
- Orion (Bell Labs)
Work in progress on an extension of Uno for C++, based on gcc.
Other tools (Code Browsers; Development Environments)
- Programming Style or Guidelines Checkers
- CodeSurfer
Supports data dependence analysis, program slicing for C,
interprocedural flow analysis. The company was co-founded by
Tom Reps.
Very well done GUI. Mostly research applications. See also CodeSonar above.
- Semantic Designs
Offers front-ends for many different languages,
Supports some flow analysis. Geared towards code transformations
or re-engineering. Targets large code bases.
Links
| |