[lkml]   [2003]   [Sep]   [10]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
Messages in this thread
SubjectCQual 0.99 Released: user/kernel pointer bug finding tool

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.

Rob Johnson

To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to
More majordomo info at
Please read the FAQ at

 \ /
  Last update: 2005-03-22 13:48    [W:0.059 / U:3.456 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site