Sciweavers

Share
VMCAI
2010
Springer

Shape Analysis of Low-Level C with Overlapping Structures

9 years 10 months ago
Shape Analysis of Low-Level C with Overlapping Structures
Abstract. Device drivers often keep data in multiple data structures simultaneously while embedding list or tree related records into the records containing the actual data; this results in overlapping structures. Shape analyses have traditionally relied on a graph-based representation of memory where a node corresponds to a whole record and edges to pointers. As this is ill-suited for encoding overlapping structures, we propose and formally relate two refined memory models. We demonstrate the appropriateness 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.
Jörg Kreiker, Helmut Seidl, Vesal Vojdani
Added 05 Mar 2010
Updated 08 Mar 2010
Type Conference
Year 2010
Where VMCAI
Authors Jörg Kreiker, Helmut Seidl, Vesal Vojdani
Comments (0)
books