swMATH ID: 10057
Software Authors: Necula, G.C., McPeak, S., Weimer, W.
Description: CCured: type-safe retrofitting of legacy code. In this paper we propose a scheme that combines type inference and run-time checking to make existing C programs type safe. We describe the CCured type system, which extends that of C by separating pointer types according to their usage. This type system allows both pointers whose usage can be verified statically to be type safe, and pointers whose safety must be checked at run time. We prove a type soundness result and then we present a surprisingly simple type inference algorithm that is able to infer the appropriate pointer kinds for existing C programs.Our experience with the CCured system shows that the inference is very effective for many C programs, as it is able to infer that most or all of the pointers are statically verifiable to be type safe. The remaining pointers are instrumented with efficient run-time checks to ensure that they are used safely. The resulting performance loss due to run-time checks is 0-150
Homepage: http://dl.acm.org/citation.cfm?id=503286
Related Software: Cyclone; DART; SLAM; Java PathFinder; z3; Coq; CIL; CUTE; Bandera; veriSoft; MOPS; SMT-LIB; Boogie; YOGI; SAFECode; BLAST; Valgrind; CESAR; FOCI; Korat
Cited in: 18 Documents

Citations by Year