Paper Info
Title
Checking the Shape Safety of Pointer Manipulations
Abstract
We present a new algorithm for checking the shape-safety of pointer manipulation programs. In our model, an abstract, data-less pointer structure is a graph. A shape is a language of graphs. A pointer manipulation program is modelled abstractly as a set of graph rewrite rules over such graphs where each rule corresponds to a pointer manipulation step. Each rule is annotated with the intended shape of its domain and range and our algorithm checks these annotations. We formally define the algorithm and apply it to a binary search tree insertion program. Shape-safety is undecidable in general, but our method is more widely applicable than previous checkers, in particular, it can check programs that temporarily violate a shape by the introduction of intermediate shape definitions.
Year
DOI
Venue
2003
10.1007/978-3-540-24771-5_5
LECTURE NOTES IN COMPUTER SCIENCE
Keywords
Field
DocType
graph rewriting,binary search tree
Tagged pointer,Pointer (computer programming),Pointer analysis,Discrete mathematics,Programming language,Function pointer,Escape analysis,Computer science,Theoretical computer science,Smart pointer,Opaque pointer,Pointer swizzling
Conference
Volume
ISSN
Citations 
3051
0302-9743
11
PageRank 
References 
Authors
0.78
8
3
Name
Order
Citations
PageRank
Adam Bakewell1746.45
Detlef Plump260462.14
Colin Runciman3907.00