The authors treat C as a dynamically typed language, but optimize away most of the runtime checks. They distinguish between SAFE pointers, SEQ pointers involving pointer arithmetic, and WILD pointers requiring full runtime checks. The CCured system supports static type checking of programs annotated with these pointer qualifiers, but, in my opinion, the most important contribution is the system’s application to existing C programs.

Section 2 presents the type system of CCured, its translation into additional information available during runtime check, and the inference algorithm for discovering the best qualifier for each pointer in legacy programs. The next section gives special attention to reducing the number of WILD pointers, by analyzing the use of casts between pointer types. Section 4 summarizes the operational semantics of a representative fragment of the language. In section 5, the authors consider some other troublesome features, such as unions, function pointers, and heap allocation. Linking transformed programs with binary libraries is discussed in section 6. In many cases, it is sufficient to write a wrapper function. The system provides the user with such functions for the most commonly used functions from the C standard library.

Sections 7 and 8 summarize some experiences. First, the authors describe the process of curing a program. Then, they present the experimental results of testing the system on real-world programs. Most programs take less than 50 percent longer to run when instrumented with CCured. An interesting point is that the tests discovered a number of bugs in well-known benchmark suites. A detailed discussion of related work, and 44 references, wraps up this clearly written paper. It can be recommended to people concerned with improving legacy system software.