Home

Welcome

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

The Checked C extension

Checked C is an opt-in extensionto C that adds bound checkng and type safety. This helps programmers write more secure and reiable code. This Wiki contains an overview of the Checked C extension and how to use it, along with suggestions for converting existing C code to Checked C. The overview is here. The detailed specification is 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.