Inferring Effective Types for Static Analysis of C Programs

Bertrand Jeannet 1, * Pascal Sotin 1, *
* 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
Abstract : The C language does not have a specific Boolean type: Boolean values are encoded with integers. This is also true for enumerated types, that may be freely and silently cast to and from integers. On the other hand, verification tools aiming at inferring the possible values of variables at each program point may benefit from the information that some (integer) variables are used solely as Boolean or enumerated type variables, or more generally as finite type variables with a small domain. Indeed, specialized and efficient symbolic representations such as BDDs may be used for representing properties on such variables, whereas approximated representations like intervals and octagons are better suited to larger domain integers and floating-points variables. Driven by this motivation, this paper proposes a static analysis for inferring more precise types for the variables of a C program, corresponding to their effective use. The analysis addresses a subset of the C99 language, including pointers, structures and dynamic allocation.
Type de document :
Communication dans un congrès
Damien Massé and Laurent Mauborgne. NSAD - Int. Workshop on Numerical and Symbolic Abstract Domains - 2011, Sep 2011, Venise, Italy. Elsevier, 288, pp.37-47, 2012, ENTCS. 〈10.1016/j.entcs.2012.10.006〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00763426
Contributeur : Bertrand Jeannet <>
Soumis le : mercredi 12 décembre 2012 - 11:15:09
Dernière modification le : jeudi 11 janvier 2018 - 01:48:47
Document(s) archivé(s) le : mercredi 13 mars 2013 - 03:51:32

Fichier

inference.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Bertrand Jeannet, Pascal Sotin. Inferring Effective Types for Static Analysis of C Programs. Damien Massé and Laurent Mauborgne. NSAD - Int. Workshop on Numerical and Symbolic Abstract Domains - 2011, Sep 2011, Venise, Italy. Elsevier, 288, pp.37-47, 2012, ENTCS. 〈10.1016/j.entcs.2012.10.006〉. 〈hal-00763426〉

Partager

Métriques

Consultations de la notice

162

Téléchargements de fichiers

72