Extending C for Checking Shape Safety

13 years 4 months ago
Extending C for Checking Shape Safety
The project Safe Pointers by Graph Transformation at the University of York has developed a method for specifying the shape of pointer-data structures by graph reduction, and a static checking algorithm for proving the shape safety of graph transformation rules modelling operations on pointer structures. In this paper, we outline how to apply this approach to the C programming language. We extend ANSI C with so-called transformers which model graph transformation rules, and with shape specifications for pointer structures. For the resulting language C-GRS, we present both ation to C and and an abstraction to graph transformation. Our main result is that the ion of transformers to graph transformation rules is correct in that the C code implementing transformers is compatible with the semantics of graph transformation.
Mike Dodds, Detlef Plump
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Authors Mike Dodds, Detlef Plump
Comments (0)