We define an automaton-based abstract interpretation of a trace semantics which identifies loops that definitely initialize all elements of an array to values satisfying a given property, a useful piece of information for the static analysis of Java-like languages. This results in a completely automatic and efficient analysis, that does not use manual code annotations. We give a formal proof of correctness that considers aspects such as side-effects of method calls. We show how the identification of those loops can be lifted to global invariants about the contents of elements of fields of array type, that hold everywhere in the code where those elements are accessed. This makes our work more significant and useful for the static analysis of real programs. The implementation of our analysis inside the Julia analyzer is both efficient and precise.
Inferring Complete Initialization of Arrays
NIKOLIC, Durica;SPOTO, Nicola Fausto
2013-01-01
Abstract
We define an automaton-based abstract interpretation of a trace semantics which identifies loops that definitely initialize all elements of an array to values satisfying a given property, a useful piece of information for the static analysis of Java-like languages. This results in a completely automatic and efficient analysis, that does not use manual code annotations. We give a formal proof of correctness that considers aspects such as side-effects of method calls. We show how the identification of those loops can be lifted to global invariants about the contents of elements of fields of array type, that hold everywhere in the code where those elements are accessed. This makes our work more significant and useful for the static analysis of real programs. The implementation of our analysis inside the Julia analyzer is both efficient and precise.File | Dimensione | Formato | |
---|---|---|---|
InferringCompleteInitializationOfArrays.pdf
accesso aperto
Tipologia:
Versione dell'editore
Licenza:
Dominio pubblico
Dimensione
1.78 MB
Formato
Adobe PDF
|
1.78 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.