Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks

Résumé

We propose a hierarchical shape abstract domain, so as to infer structural invariants of dynamic structures such as lists living inside static structures, such as arrays. This programming pattern is often used in safety critical embedded software that need to ''allocate'' dynamic structures inside static regions due to dynamic memory allocation being forbidden in this context. Our abstract domain precisely describes such hierarchies of structures. It combines several instances of simple shape abstract domains, dedicated to the representation of elementary shape properties, and also embeds a numerical abstract domain. This modular construction greatly simplifies the design and the implementation of the abstract domain. We provide an implementation, and show the effectiveness of our approach on a problem taken from a real code.
Fichier principal
Vignette du fichier
aplas12.pdf (216.8 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00760427 , version 1 (08-01-2013)

Identifiants

Citer

Pascal Sotin, Xavier Rival. Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks. APLAS 2012 - Asian Conference on Programming Languages And Software, Dec 2012, Kyoto, Japan. pp.131-147, ⟨10.1007/978-3-642-35182-2_10⟩. ⟨hal-00760427⟩
141 Consultations
179 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More