Interprocedural analyses: a comparison
Identifieur interne : 002240 ( Main/Merge ); précédent : 002239; suivant : 002241Interprocedural analyses: a comparison
Auteurs : Helmut Seidl [Allemagne] ; Christian Fecht [Allemagne]Source :
- The Journal of Logic Programming [ 0743-1066 ] ; 2000.
Abstract
We present a framework for program analysis of languages with procedures which is general enough to allow for a comparison of various approaches to interprocedural analysis. Our framework is based on a small-step operational semantics and subsumes both frameworks for imperative and for logic languages. We consider reachability analysis, that is, the problem of approximating the sets of program states reaching program points. We use our framework in order to clarify the impact of several independent design decisions on the precision of the analysis. Thus, we compare intraprocedural forward accumulation with intraprocedural backward accumulation. Furthermore, we consider both relational and functional approaches. While for relational analysis the accumulation strategy makes no difference in precision, we prove for functional analysis that forward accumulation may lose precision against backward accumulation. Concerning the relative precision of relational analyses and corresponding functional analyses, we exhibit scenarios where functional analysis does not lose precision. Finally, we explain why even an enhancement of functional analysis through disjunctive completion of the underlying abstract domain may sometimes lose precision against relational analysis.
Url:
DOI: 10.1016/S0743-1066(99)00058-8
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001663
- to stream Istex, to step Curation: 001551
- to stream Istex, to step Checkpoint: 000C64
Links to Exploration step
ISTEX:9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Interprocedural analyses: a comparison</title>
<author><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name>
</author>
<author><name sortKey="Fecht, Christian" sort="Fecht, Christian" uniqKey="Fecht C" first="Christian" last="Fecht">Christian Fecht</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802</idno>
<date when="2000" year="2000">2000</date>
<idno type="doi">10.1016/S0743-1066(99)00058-8</idno>
<idno type="url">https://api.istex.fr/document/9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802/fulltext/pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001663</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001663</idno>
<idno type="wicri:Area/Istex/Curation">001551</idno>
<idno type="wicri:Area/Istex/Checkpoint">000C64</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000C64</idno>
<idno type="wicri:doubleKey">0743-1066:2000:Seidl H:interprocedural:analyses:a</idno>
<idno type="wicri:Area/Main/Merge">002240</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a">Interprocedural analyses: a comparison</title>
<author><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name>
<affiliation wicri:level="1"><country xml:lang="fr">Allemagne</country>
<wicri:regionArea>FB IV – Informatik, Universität Trier, D-54286 Trier</wicri:regionArea>
<wicri:noRegion>54286 Trier</wicri:noRegion>
<wicri:noRegion>D-54286 Trier</wicri:noRegion>
</affiliation>
<affiliation></affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Fecht, Christian" sort="Fecht, Christian" uniqKey="Fecht C" first="Christian" last="Fecht">Christian Fecht</name>
<affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country>
<wicri:regionArea>Universität des Saarlandes, Postfach 151150, D-66041 Saarbrücken</wicri:regionArea>
<placeName><region type="land" nuts="2">Sarre (Land)</region>
<settlement type="city">Sarrebruck</settlement>
</placeName>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">The Journal of Logic Programming</title>
<title level="j" type="abbrev">JLP</title>
<idno type="ISSN">0743-1066</idno>
<imprint><publisher>ELSEVIER</publisher>
<date type="published" when="2000">2000</date>
<biblScope unit="volume">43</biblScope>
<biblScope unit="issue">2</biblScope>
<biblScope unit="page" from="123">123</biblScope>
<biblScope unit="page" to="156">156</biblScope>
</imprint>
<idno type="ISSN">0743-1066</idno>
</series>
<idno type="istex">9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802</idno>
<idno type="DOI">10.1016/S0743-1066(99)00058-8</idno>
<idno type="PII">S0743-1066(99)00058-8</idno>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0743-1066</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We present a framework for program analysis of languages with procedures which is general enough to allow for a comparison of various approaches to interprocedural analysis. Our framework is based on a small-step operational semantics and subsumes both frameworks for imperative and for logic languages. We consider reachability analysis, that is, the problem of approximating the sets of program states reaching program points. We use our framework in order to clarify the impact of several independent design decisions on the precision of the analysis. Thus, we compare intraprocedural forward accumulation with intraprocedural backward accumulation. Furthermore, we consider both relational and functional approaches. While for relational analysis the accumulation strategy makes no difference in precision, we prove for functional analysis that forward accumulation may lose precision against backward accumulation. Concerning the relative precision of relational analyses and corresponding functional analyses, we exhibit scenarios where functional analysis does not lose precision. Finally, we explain why even an enhancement of functional analysis through disjunctive completion of the underlying abstract domain may sometimes lose precision against relational analysis.</div>
</front>
</TEI>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002240 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 002240 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Rhénanie |area= UnivTrevesV1 |flux= Main |étape= Merge |type= RBID |clé= ISTEX:9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802 |texte= Interprocedural analyses: a comparison }}
![]() | This area was generated with Dilib version V0.6.31. | ![]() |