CQual 0.99 Released: user/kernel pointer bug finding tool

["Robert T. Johnson" <rtjohnso@eecs.berkeley.edu>]

Download: http://www.cs.umd.edu/~jfoster/cqual/.
Support:  cqual@cs.umd.edu.

CQual is a program verification tool that uses type-qualifier
inference to find bugs in C programs.  This release of CQual includes
support for finding user/kernel pointer bugs in the linux kernel.
CQual has already found user/kernel pointer bugs in source files that
passed through Linus' "sparse" tool without generating any warnings.
Our goals with this release are

- help kernel developers avoid user/kernel bugs
- get feedback from kernel developers for future CQual features

CQual's current main features are:

- It requires _very_ few annotations: we currently use only ~200
- It's sound: CQual verifies the _absence_ of user/kernel bugs
- It generates fewer false warnings than sparse.
- It's context-sensitve: CQual doesn't confuse different calls to the 
  same function.
- CQual allows different instances of a struct type to hold different 
  kinds of pointers (i.e. user vs. kernel)
- It can be easily extended to find new types of bugs by editing a 
  configuration file
- It's fast: CQual analyzes most files in 1-2 seconds.
- It integrates easily into the kernel checking process.

The distribution contains a KERNEL-QUICKSTART to help kernel
developers start finding user/kernel bugs quickly.  We look forward to
hearing your feedback.

CQual is currently developed by Jeff Foster, John Kodumal, Tachio
Terauchi, Rob Johnson, and many others.

Best,
Rob Johnson