Inferring Effective Types for Static Analysis of C Programs

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.