Inference of field initialization

Download: PDF.

“Inference of field initialization” by Fausto Spoto and Michael D. Ernst. University of Washington Department of Computer Science and Engineering technical report UW-CSE-10-02-01, (Seattle, WA, USA), February 6, 2010.


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-null. 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.

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.

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.

Download: PDF.

BibTeX entry:

   author = {Fausto Spoto and Michael D. Ernst},
   title = {Inference of field initialization},
   institution = {University of Washington Department of Computer Science
	and Engineering},
   number = {UW-CSE-10-02-01},
   address = {Seattle, WA, USA},
   month = {February~6,},
   year = {2010}

(This webpage was created with bibtex2web.)

Back to Program Analysis Group publications.