Messages in this thread | | | Subject | CQual 0.99 Released: user/kernel pointer bug finding tool | From | "Robert T. Johnson" <> | Date | 10 Sep 2003 16:02:08 -0700 |
| |
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
- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/
| |