作者: George C. Necula , Scott McPeak , Westley Weimer
关键词: Pointer (computer programming) 、 Programming language 、 Soundness 、 Operational semantics 、 Data structure 、 Computer science 、 Type inference 、 Legacy code 、 Dangling pointer 、 Memory safety 、 Software 、 Computer Graphics and Computer-Aided Design
摘要: In this paper we propose a scheme that combines type inference and run-time checking to make existing C programs safe. We describe the CCured system, which extends of by separating pointer types according their usage. This system allows both pointers whose usage can be verified statically safe, safety must checked at run time. prove soundness result then present surprisingly simple algorithm is able infer appropriate kinds for programs.Our experience with shows very effective many programs, as it most or all are verifiable The remaining instrumented efficient checks ensure they used safely. resulting performance loss due 0-150%, several times better than comparable approaches use only dynamic checking. Using have discovered programming bugs in established such SPECINT95 benchmarks.