Home

Welcome

Welcome to the Wiki for Checked C! This Wiki is current and actively maintained as of July 2023.

The Checked C extension

Checked C is an opt-in extension to C that adds bound checking and type safety. This helps programmers write more secure and reliable code. This Wiki contains:

• An overview of the Checked C extension and how to use it.
• Suggestions for converting existing C code to Checked C.

For developers with existing C codebases, 3C (Checked-C-Convert) software facilitates the transition to Checked C by inferring as many Checked C annotations as possible and guiding you through the assignment of the remaining ones. A detailed specification is here.

For a deeper understanding of 3C, refer to the 3C documentation. Note that 3C is in its pre-alpha stage as of March 2021, but is under active development.

A detailed specification is available here.

Example code

• For some simple code, see the samples directory.

• For some more complicated examples, see our Checked C translations of the Olden and PtrDist benchmarks.

• To see some real-world C code that has been converted to Checked C, see

  • The Checked C fork of the parson JSon parser.
  • The Checked C branch of the Microsoft Research Robust Internet of Things (RIoT) project. In this branch, the cryptography code has been converted to use Checked C.

  -For some in-progress conversions to Checked C, see the conversions of one of the following code bases to Checked C:

  1. Vsftpd (re-port branch)
  2. Lua (checkedc-port branch)
  3. The Checked C fork of the musl C library.
  4. The Checked C fork of libc-test. Used to test the conversion of musl to Checked C.

Compiler

To use Checked C, currently you need to build your own copy of the compiler. Directions are here.

Participating

Checked C is an open-source research project. Anyone with time or interest can participate. Trying out Checked C, reporting bugs, and giving us feedback is helpful. There are other ways to contribute too.