Extending C for Checking Shape Safety |
| |
Authors: | Mike Dodds Detlef Plump |
| |
Affiliation: | The University of York, UK |
| |
Abstract: | 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 a translation to C and and an abstraction to graph transformation. Our main result is that the abstraction of transformers to graph transformation rules is correct in that the C code implementing transformers is compatible with the semantics of graph transformation. |
| |
Keywords: | Pointer programming shape safety C graph transformation |
本文献已被 ScienceDirect 等数据库收录! |
|