Jörg Kreiker, Helmut Seidl and Vesal Vojdani. Shape Analysis of Low-Level C with Overlapping Structures. In Gilles Barthe and Manuel V. Hermenegildo, editors, Verification, Model Checking, and Abstract Interpretation, volume 5944 of Lecture Notes in Computer Science, pages 214-230, Madrid, Spain, January 2010. Springer.

Device drivers often keep data in multiple data structures si- multaneously while embedding list or tree related records into the records containing the actual data; this results in overlapping structures. Shape nalyses have traditionally relied on a graph-based representation of memory where a node corresponds to a whole record and edges to point- ers. As this is ill-suited for encoding overlapping structures, we propose and formally relate two refined memory models. We demonstrate the ap- propriateness of these models by implementing shape analyses based on them within the TVLA framework. The implementation is exemplified using code extracted from cache managing kernel modules.

Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com