CQual 0.99 Released: user/kernel pointer bug finding tool
From: Robert T. Johnson
Date: Wed Sep 10 2003 - 18:03:55 EST
Download: http://www.cs.umd.edu/~jfoster/cqual/.
Support: cqual@xxxxxxxxxxx
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
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
Please read the FAQ at http://www.tux.org/lkml/