Skip to Main content Skip to Navigation
Journal articles

Control-flow analysis of function calls and returns by abstract interpretation

Jan Midtgaard 1 Thomas Jensen 2
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Abstract interpretation techniques are used to derive a control-flow analysis for a simple higher-order functional language. The analysis approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. The analysis is systematically derived by abstract interpretation of a stack-based abstract machine using a series of Galois connections. We prove that the analysis is equivalent to an analysis obtained by first transforming the program into continuation-passing style and then performing control flow analysis of the transfored program. We then show how the analysis induces an equivalent constraint-based formulation, thereby providing a rational reconstruction of a constraint-based CFA from abstract interpretation principles.
Document type :
Journal articles
Complete list of metadatas

Cited literature [43 references]  Display  Hide  Download

https://hal.inria.fr/hal-00758152
Contributor : Thomas Jensen <>
Submitted on : Thursday, November 29, 2012 - 1:22:59 PM
Last modification on : Friday, July 10, 2020 - 4:21:54 PM
Long-term archiving on: : Saturday, December 17, 2016 - 4:10:39 PM

File

artikel.pdf
Files produced by the author(s)

Identifiers

Citation

Jan Midtgaard, Thomas Jensen. Control-flow analysis of function calls and returns by abstract interpretation. Information and Computation, Elsevier, 2012, 2012, pp.49-76. ⟨10.1016/j.ic.2011.11.005⟩. ⟨hal-00758152⟩

Share

Metrics

Record views

1977

Files downloads

372