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.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Mike Dodds, Detlef Plump
• Keywords: ENTCS 2006, Graph Transformation, Graph Transformation Rules, Pointer Structures