The important result is in Table 1 of the actual paper.[2] The converter looks at pointers, and classifies them as "pointer", "array of known size", or "unknown". "Unknown" ranges from 49% to 76%. You can't convert an existing code base automatically with that low a success rate.
The big design mistake in C was "pointer" and "array" being the same thing syntactically. Trying to undo that has taken decades.
Their converter is on Github.[3] This is a Microsoft project.
The syntax they use is rather clunky:
void copy(char ∗dst : bytecount(n),
const char ∗src : bytecount(n),
size_t n);
That's halfway between C and Pascal/Ada/Rust.I proposed more C-like syntax like this:
void copy(size_t n, char (&a)[n], const char (&b)[n])
It's annoying that you need the parentheses, but that's C/C++ syntax.I wanted to put C++ style references into C so you could pass arrays as arrays, rather than degrading them to pointers. I also wanted to add slices of arrays, so you could pass a slice of an array as an array. Those are standard features of most later languages, and handle most of the cases for which pointer arithmetic is used. C doesn't have the expressive power to even talk about those things unambiguously. So they can't be checked either at compile time or run time.
The hard job is converting legacy code by automatically inferring the information that C source code lacks. It's good that they're trying. But a 50% success rate indicates they're just getting the easy hits. If anybody ever gets a good array size inference system, it would be a huge win. Then existing C could be converted to something better. Not necessarily "Checked C". Rust or Go would be options.
[1] http://www.animats.com/papers/languages/safearraysforc43.pdf