Inferring Effective Types for Static Analysis of C Programs - 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

Inferring Effective Types for Static Analysis of C Programs

Résumé

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.
Fichier principal
Vignette du fichier
inference.pdf (188.52 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00763426 , version 1 (12-12-2012)

Identifiants

Citer

Bertrand Jeannet, Pascal Sotin. Inferring Effective Types for Static Analysis of C Programs. NSAD - Int. Workshop on Numerical and Symbolic Abstract Domains - 2011, Sep 2011, Venise, Italy. pp.37-47, ⟨10.1016/j.entcs.2012.10.006⟩. ⟨hal-00763426⟩
94 Consultations
100 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More