Safe programming at the c level of abstraction

摘要: Memory safety and type are invaluable features for building robust software. However, most safe programming languages at a high level of memory management. This control is one reason C remains the de facto standard writing systems software or extending legacy already written in C. The Cyclone language aims to bring C-style without sacrificing programmer necessary low-level A combination advanced compile-time techniques, run-time checks, modern helps achieve this goal. This dissertation focuses on techniques. system with quantified types effects prevents incorrect casts, dangling-pointer dereferences, data races. An intraprocedural flow analysis dereferencing NULL pointers uninitialized memory, extensions it can prevent proofs demonstrate that these techniques sound: violations they address become impossible. A less formal evaluation establishes two other design goals equal importance. First, expressive. Although rejects some programs, permits many idioms regarding generic code, manual management, lock-based synchronization, NULL-pointer checking, initialization. Second, represents unified approach. small collection addresses range problems, indicating problems more alike than originally seem.