CCured in the real world

CCured is a program transformation system that adds memory safety guarantees to C programs by verifying statically that memory errors cannot occur and by inserting run-time checks where static verification is insufficient. This paper addresses major usability issues in a previous version of CCured, in which many type casts required the use of pointers whose representation was expensive and incompatible with precompiled libraries. We have extended the CCured type inference algorithm to recognize and verify statically a large number of type casts; this goal is achieved by using physical subtyping and pointers with run-time type information to allow parametric and subtype polymorphism. In addition, we present a new instrumentation scheme that splits CCured’s metadata into a separate data structure whose shape mirrors that of the original user data. This scheme allows instrumented programs to invoke external functions directly on the program’s data without the use of a wrapper functi...

• Type: Conference
• Year: 2003
• Where: PLDI
• Authors: Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, Westley Weimer
• Keywords: CCured Type Inference, PLDI 2003, Programming Languages, Run-time Type Information, Type Casts