Compile-Time Debugging of C Programs Working on Trees

We exhibit a technique for automatically verifying the safety of simple C programs working on tree-shaped data structures. We do not consider the complete behavior of programs, but only attempt to verify that they respect the shape and integrity of the store. A verified program is guaranteed to preserve the tree-shapes of data structures, to avoid pointer errors such as NULL dereferences, leaking memory, and dangling references, and furthermore to satisfy assertions specified in a specialized store logic. A program is transformed into a single formula in WSRT, a novel extension of WS2S that is decided by the MONA tool. This technique is complete for loop-free code, but for loops and recursive functions we rely on Hoare-style invariants. A default well-formedness invariant is supplied and can be strengthened as needed by programmer annotations. If a program fails to verify, a counterexample in the form of an initial store that leads to an error is automatically generated. This extends p...

• Type: Conference
• Year: 2000
• Where: ESOP
• Authors: Jacob Elgaard, Anders Møller, Michael I. Schwartzbach
• Keywords: Data Structures, ESOP 2000, Programming Languages, Specialized Store Logic, Tree-shaped Data Structures