Inference of field initialization
Submitted by mernst on Wed, 2011-11-30 14:35
| Title | Inference of field initialization |
| Publication Type | Miscellaneous |
| Year of Publication | 2010 |
| Authors | Spoto F, Ernst MD |
| Abstract | <p>A raw object is partially initialized, with only some of its fields set to legal values. A raw object may violate its object invariants, such as that a given field is non-<tt>null</tt>. Programs often need to manipulate partially-initialized objects, but they must do so with care. Furthermore, analyses must be aware of rawness. For instance, software verification cannot depend on object invariants for raw objects. </p> <p> We present a static analysis that infers a safe over-approximation of the program variables, fields, or array elements that, at runtime, might hold non-fully initialized objects. Our formalization is flow-sensitive and considers the exception flow in the analyzed programs. We have proved the analysis to be sound. </p> <p> We have also implemented our analysis, in a tool called Julia that computes both nullness and rawness information. We have evaluated Julia on over 50K lines of code. We have compared its output to manually-written nullness and rawness information, and to an independently-written type-checking tool that checks nullness and rawness. Julia's output is accurate and, we believe, useful both to programmers and to static analyses.</p> |
| Downloads | |
| Citation Key | SpotoE2010:TR |
Last changed Mon, 2013-06-03 10:27

cs.