-
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
|
|
