A Memory Model for Static Analysis of C Programs

被引：44
|
作者：
Xu, Zhongxing [1 ]
Kremenek, Ted [2 ]
Zhang, Jian [1 ]
机构：
[1] Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing 100864, Peoples R China
[2] Apple Inc, Beijing 100864, Peoples R China
来源：
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT I | 2010年 / 6415卷
基金：
中国国家自然科学基金;
关键词：
D O I：
10.1007/978-3-642-16558-0_44
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Automatic bug finding with static analysis requires precise tracking of different memory object values. This paper describes a memory modeling method for static analysis of C programs. It is particularly suitable for precise path-sensitive analyses, e.g., symbolic execution. It can handle almost all kinds of C expressions, including arbitrary levels of pointer dereferences, pointer arithmetic, composite array and struct data types, arbitrary type casts, dynamic memory allocation, etc. It maps aliased lvalue expressions to the identical object without extra alias analysis. The model has been implemented in the Clang static analyzer and enhanced the analyzer a lot by enabling it to have precise value tracking ability.
引用
收藏
页码：535 / +
页数：3
相关论文
共 50 条
  • [1] A sound abstract memory model for static analysis of C programs
    Dong, Yukun
    INTERNATIONAL JOURNAL OF COMPUTATIONAL SCIENCE AND ENGINEERING, 2018, 16 (03) : 255 - 264
  • [2] Static analysis of C programs via region-based memory model
    Dong, Yu-Kun
    Jin, Da-Hai
    Gong, Yun-Zhan
    Xing, Ying
    Ruan Jian Xue Bao/Journal of Software, 2014, 25 (02): : 357 - 372
  • [3] Static Analysis of Lockless Microcontroller C Programs
    Beckschulze, Eva
    Biallas, Sebastian
    Kowalewski, Stefan
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (102): : 103 - 114
  • [4] A Library Modeling Language for the Static Analysis of C Programs
    Ouadjaout, Abdelraouf
    Mine, Antoine
    STATIC ANALYSIS (SAS 2020), 2020, 12389 : 223 - 247
  • [5] SharpChecker: Static analysis tool for C# programs
    Koshelev, V. K.
    Ignatiev, V. N.
    Borzilov, A. I.
    Belevantsev, A. A.
    PROGRAMMING AND COMPUTER SOFTWARE, 2017, 43 (04) : 268 - 276
  • [6] Modular Static Analysis of String Manipulations in C Programs
    Journault, Matthieu
    Mine, Antoine
    Ouadjaout, Abdelraouf
    STATIC ANALYSIS (SAS 2018), 2018, 11002 : 243 - 262
  • [7] SharpChecker: Static analysis tool for C# programs
    V. K. Koshelev
    V. N. Ignatiev
    A. I. Borzilov
    A. A. Belevantsev
    Programming and Computer Software, 2017, 43 : 268 - 276
  • [8] Inferring Effective Types for Static Analysis of C Programs
    Jeannet, Bertrand
    Sotin, Pascal
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2012, 288 : 37 - 47
  • [9] Verified Compilation of C Programs with a Nominal Memory Model
    Wang, Yuting
    Zhang, Ling
    Shao, Zhong
    Koenig, Jeremie
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2022, 6 (POPL):
  • [10] Type Inference for C: Applications to the Static Analysis of Incomplete Programs
    Melo, Leandro T. C.
    Ribeiro, Rodrigo G.
    Guimaraes, Breno C. F.
    Quintao Pereira, Fernando Magno
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2020, 42 (03):
12345