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:
@techreport{SpotoE2010:TR,
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.