Deputy is a C compiler that is capable of preventing common C programming errors, including out-of-bounds memory accesses as well as many other common type-safety errors. It is designed to work on real-world code, up to and including the Linux kernel itself.
Deputy allows C programmers to provide simple type annotations that describe pointer bounds and other important program invariants. Deputy verifies that your program adheres to these invariants through a combination of compile-time and run-time checking.
Unlike other tools for checking C code, Deputy provides a flexible annotation language that allows you to describe many common programming idioms without changing your data structures. As a result, using Deputy requires less programmer effort than other tools. In fact, code compiled with Deputy can be linked directly with code compiled by other C compilers, so you can choose exactly when and where to use Deputy within your C project.
Deputy is implemented using the CIL infrastructure for C program analysis and transformation, and it uses GCC as a back end.
Deputy 1.1 is available in the following formats:
In addition, the latest build is available via anonymous access to our Subversion repository:
svn://hal.cs.berkeley.edu/home/svn/projects/trunk/deputy
If you choose to download the source distribution or check out from the Subversion repository, you will need the OCaml compiler to build Deputy.
Deputy is currently being developed for Linux, Cygwin, FreeBSD, and Mac OS X on 32-bit x86 processors. Other platforms and processors should work as well but may require additional effort to build. (Please feel free to submit comments and/or patches for other platforms!)
We've started a mailing list for users of Deputy. Please feel free to send comments, suggestions, and bug reports to this list. We will also send updates to this list when new versions are released.
You can subscribe, browse the archives, or simply send mail to deputy@deputy.cs.berkeley.edu.
Further information about Deputy and its uses can be found in the following papers:
Deputy was written by Jeremy Condit, Matt Harren, Zach Anderson, and George Necula. Many thanks to Feng Zhou, Rob Ennals, David Gay, Ilya Bagrak, Bill McCloskey, and Eric Brewer for valuable discussions and feedback. Thanks to Kevin Lo for the FreeBSD port.