Interprocedural Pointer Analysis in Goanna

被引：3

作者：

Brauer, Joerg ^{[2
]}

Huuck, Ralf ^{[1
]}

Schlich, Bastian ^{[2
]}

机构：

[1] Univ New South Wales, Natl ICT Australia Ltd NICTA, Locked Bag 6016, Sydney, NSW 1466, Australia

[2] Rhein Westfal TH Aachen, Embedded Software Lab, D-52074 Aachen, Germany

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2009年 / 254卷 / 65-83期

基金：

澳大利亚研究理事会;

关键词：

Static Analysis; Interprocedural Analysis; Model Checking; Pointer Analysis;

D O I：

10.1016/j.entcs.2009.09.060

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Goanna is an industrial-strength static analysis tool used in academia and industry alike to find bugs in C/C++ programs. Unlike existing approaches, Goanna uses the off-the-shelf model checker NuSMV as its core analysis engine on a syntactic flow-sensitive program abstraction. The CTLbased model checking approach enables a high degree of flexibility in writing checks and scales to large code bases. In this paper, a new approach to pointer analysis for C is described. It is detailed how this technique is integrated into the model checking approach in order to perform interprocedural analysis. The performance and precision of this approach are demonstrated using a case study.

引用

页码：65 / 83

页数：19

共 24 条

[1]

Andersen L.O., 1994, THESIS

[2] THE TEMPORAL LOGIC OF BRANCHING TIME [J].

BENARI, M ;

PNUELI, A ;

MANNA, Z .

ACTA INFORMATICA, 1983, 20 (03) :207-226

[3] Modular interprocedural pointer analysis using access paths: Design, implementation, and evaluation [J].

Cheng, BC ;

Hwu, WMW .

ACM SIGPLAN NOTICES, 2000, 35 (05) :57-69

[4]

Choi J. -D., 1993, PRINCIPLES PROGRAMMI

[5]

Clarke E., 2000, LNCS, V1855, P154, DOI [10.1007/10722167_15, DOI 10.1007/10722167_15]

[6]

Clarke EM, 1999, MODEL CHECKING, P1

[7] EFFICIENTLY COMPUTING STATIC SINGLE ASSIGNMENT FORM AND THE CONTROL DEPENDENCE GRAPH [J].

CYTRON, R ;

FERRANTE, J ;

ROSEN, BK ;

WEGMAN, MN ;

ZADECK, FK .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1991, 13 (04) :451-490

[8] Unification-based pointer analysis with directional assignments [J].

Das, M .

ACM SIGPLAN NOTICES, 2000, 35 (05) :35-46

[9]

DEUTSCH A, 1994, SIGPLAN NOTICES, V29, P230, DOI 10.1145/773473.178263

[10]

EMAMI M, 1994, SIGPLAN NOTICES, V29, P242, DOI 10.1145/773473.178264

← 1 2 3 →