Create stand-alone tool for checking Checked C programs compiled with regular C compilers.

[dtarditi]

People interested in Checked C may not be willing to switch to the Checked C clang compiler.

• They may be working on an existing project that does not use clang.
• They may be compiling for a computer architecture not supported by clang, such as a specialized embedded processor.
• They may not want to take a critical dependency on a research compiler or a non-standard version of clang.

For this scenario, we would like to create a "Checked C Static Checker" (name suggestions are welcome). This tool will check that no runtime checks are needed to enforce Checked C semantics (that is, all checks that would be inserted by the Checked C compiler are redundant to existing checks in the programs).

Programmers could then use this checker to check programs written using the erasable Checked C syntax. For their production compiler, the syntax would automatically be erased.

One question to address: can we identify some people who will use Checked C if such a tool exists? One concern is how faithfully the tool models the semantics of C as implemented by the production compiler they use. We will base this tool on the current Checked C clang implementation. At the very least, we need to make primitive type sizes line up and to look at known ambiguities in the C language specification. It will be good to work through those issues with a a concrete production compiler in mind.

[dtarditi]

UEFI developers are a good target for this tool. They primarily use GCC to compile UEFI, although the code also compiles with clang. Clang matches GCC's C semantics well. This will simplify the initial implementation of the tool.