Inferring Effective Types for Static Analysis of C Programs - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2012

Inferring Effective Types for Static Analysis of C Programs

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.
Fichier principal
Vignette du fichier
inference.pdf (188.52 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

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

Identifiers

Cite

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 View
100 Download

Altmetric

Share

Gmail Facebook X LinkedIn More