Concrete Memory Models for Shape Analysis

This paper discusses four store-based concrete memory models. We characterize memory models by the class of pointers they support and whether they use numerical or symbolic offsets to address values in a block. We give the semantics of a C-like language within each of these memory models to illustrate their differences. The language we consider is a fragment of Leroy's Clight, including arrays, pointer arithmetics but excluding casts. All along the paper, we link these concrete memory models with existing shape analyses.