Concrete Memory Models for Shape Analysis

Pascal Sotin 1, * Bertrand Jeannet 1, * Xavier Rival 2
* Auteur correspondant
1 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 ABSTRACTION - Abstract Interpretation and Static Analysis
CNRS - Centre National de la Recherche Scientifique : UMR 8548, Inria Paris-Rocquencourt, DI-ENS - Département d'informatique de l'École normale supérieure
Abstract : 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.
Type de document :
Communication dans un congrès
NSAD'2010 - Second International Workshop on Numerical and Symbolic Abstract Domains, Sep 2010, Perpignan, France. Elsevier, 267, pp.139--150, 2010, 〈10.1016/j.entcs.2010.09.012〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00786330
Contributeur : Bertrand Jeannet <>
Soumis le : vendredi 8 février 2013 - 13:36:09
Dernière modification le : vendredi 25 mai 2018 - 12:02:05

Lien texte intégral

Identifiants

Collections

Citation

Pascal Sotin, Bertrand Jeannet, Xavier Rival. Concrete Memory Models for Shape Analysis. NSAD'2010 - Second International Workshop on Numerical and Symbolic Abstract Domains, Sep 2010, Perpignan, France. Elsevier, 267, pp.139--150, 2010, 〈10.1016/j.entcs.2010.09.012〉. 〈hal-00786330〉

Partager

Métriques

Consultations de la notice

226