A framework for the static verification of API calls

被引:6
作者
Spinellis, Diomidis [1 ]
Louridas, Panagiotis [1 ]
机构
[1] Athens Univ Economist & Business, Dept Management Sci & Technol, GR-10434 Athens, Greece
关键词
static analysis; API; library; programming by contract; FindBugs;
D O I
10.1016/j.jss.2006.09.040
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
A number of tools can statically check program code to identify commonly encountered bug patterns. At the same time, programs are increasingly relying on external APIS for performing the bulk of their work: the bug-prone program logic is being fleshed-out, and many errors involve tricky subroutine calls to the constantly growing set of external libraries. Extending the static analysis tools to cover the available APIS is an approach that replicates scarce human effort across different tools and does not scale. Instead, we propose moving the static API call verification code into the API implementation, and distributing the verification code together with the library proper. We have designed a framework for providing static verification code together with Java classes, and have extended the FindBugs static analysis tool to check the corresponding method invocations. To validate our approach we wrote verification tests for 100 different methods, and ran FindBugs on 6.9 million method invocations on what amounts to about 13 million lines of production-quality code. In the set of 55 thousand method invocations that could potentially be statically verified our approach identified 800 probable errors. (C) 2006 Elsevier Inc. All rights reserved.
引用
收藏
页码:1156 / 1168
页数:13
相关论文
共 54 条
  • [1] [Anonymous], 2001, Symposium on Operating Systems Principles
  • [2] [Anonymous], 65 BELL LAB
  • [3] [Anonymous], ICSE 81
  • [4] Arnold K., 2006, JAVA PROGRAMMING LAN
  • [5] Combining test case generation and runtime verification
    Artho, C
    Barringer, H
    Goldberg, A
    Havelund, K
    Khurshid, S
    Lowry, M
    Pasareanu, C
    Rosu, G
    Sen, K
    Visser, W
    Washington, R
    [J]. THEORETICAL COMPUTER SCIENCE, 2005, 336 (2-3) : 209 - 234
  • [6] Ball Thomas, 2004, Technical Report MSR-TR-2004-08
  • [7] Ball VE, 2002, STUD PRODUCT EFF, V2, P1
  • [8] Barach D. R., 1982, SIGPLAN Notices, V17, P32, DOI 10.1145/988376.988379
  • [9] BARRINGER H, 2006, ELECT NOTES THEORETI, V144
  • [10] Beck K, 1998, JAVA REP, V3, P37