CCured
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 sysiem allows both pointers whose usage can be verif...
| Published in: | ACM SIGPLAN Notices |
|---|---|
| Main Authors: | , , |
| Format: | Article in Journal/Newspaper |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2012
|
| Subjects: | |
| Online Access: | http://dx.doi.org/10.1145/2442776.2442786 https://dl.acm.org/doi/pdf/10.1145/2442776.2442786 |
| Summary: | 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 sysiem 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 algoriihm that is able lo infer the appropriate pointer kinds for existing C programs. Our experience wiih the CCured sysiem 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 wiih efficient run-time checks to ensure that they are used safely. The resulting performance loss due to run-time checks is 0-150%, which is several times better than comparable approaches thai use only dynamic checking. Using CCured we have discovered programming bugs in established C programs such as several SPECINT95 benchmarks. |
|---|