CCured swMATH ID: 10057 Software Authors: Necula, George C.; McPeak, Scott; Weimer, Westley 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: SLAM; DART; Java PathFinder; Cyclone; CUTE; z3; Bandera; veriSoft; Coq; CIL; MOPS; Boogie; YOGI; CESAR; SMT-LIB; SAFECode; BLAST; Valgrind; FOCI; Korat Cited in: 18 Documents all top 5 Cited by 37 Authors 3 Godefroid, Patrice 3 Necula, George C. 3 Weimer, Westley 2 Barrett, Clark W. 2 McPeak, Scott 1 Condit, Jeremy 1 Conway, Christopher L. 1 Dams, Dennis René 1 Della Penna, Giuseppe 1 Frolov, Alexei M. 1 Hackett, Brian 1 Horwitz, Susan 1 Jhala, Ranjit 1 Klarlund, Nils 1 Krandick, Werner 1 Lahiri, Shuvendu Kumar 1 Majumdar, Rupak 1 Matousek, Tomas 1 Morrisett, Greg 1 Namjoshi, Kedar S. 1 Nori, Aditya Vithal 1 Oiwa, Yutaka 1 Qadeer, Shaz 1 Rahul, Shree P. 1 Rajamani, Sriram K. 1 Richardson, David G. 1 Sekiguchi, Tatsurou 1 Sen, Koushik 1 Smith, Michael J. A. 1 Sumii, Eijiro 1 Tetali, Sai Deep 1 Wang, Wei 1 Wies, Thomas 1 Xu, Ru-Gang 1 Yonezawa, Akinori 1 Yong, Suan Hsi 1 Zavoral, Filip Cited in 3 Serials 1 Programming and Computer Software 1 Formal Methods in System Design 1 Computer Languages, Systems & Structures Cited in 1 Field 18 Computer science (68-XX) Citations by Year