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.
Deputy is currently available as a Debian package, an RPM, or a source distribution:
If you choose to download the source distribution, you will need the OCaml compiler to build Deputy.
Deputy is currently being developed for Linux and Cygwin on 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!)
Further information about Deputy and its uses can be found in the following papers:
Please send questions and feedback to the Deputy team at deputy@deputy.cs.berkeley.edu. We welcome any comments you have about your experience using Deputy and your suggestions for improving it!
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.