基于有界模型检测的C/C++程序内存泄露检测  

C/C ++ program memory leak detection based on bounded model checking

作　　者：黄蔚[1] 洪玫[1] 杨秋辉[1] 郭鑫宇[1] 代声馨[1] 徐保平[1] 高婉玲 赵鹤[1] 

机构地区：[1]四川大学计算机学院,成都610065

出　　处：《计算机应用研究》2016年第6期1762-1766,共5页Application Research of Computers

基　　金：四川省应用基础研究项目(2014JY0112)

摘　　要：C/C++语言中的动态内存管理机制自由且灵活,但动态内存的使用容易引入内存泄露,导致系统性能降低甚至系统崩溃。为了更加有效地检测内存泄露,提出了一个基于有界模型检测技术的C/C++程序内存泄露检测方案MLD-CBMC。该方案以C/C++程序文件为输入,利用有界模型检测技术对程序进行展开处理,加入内存泄露性质,并利用可满足性模理论(SMT)对程序约束和性质组成的验证条件编码,使用SMT求解器对验证条件求解,将检测内存泄露问题转换为求解可满足性问题,实现C/C++程序内存泄露的检测。通过实验验证了方案的有效性,并与其他有界模型检测工具进行对比实验,实验证明方案对内存泄露的检测能力更强。The dynamic memory management mechanism in C / C ＋＋ programming language is free and flexible,but when used by developer it is easy to introduce memory leaks which lead to performance degradation and even failure of system. In order to detect memory leak more effectively,this paper proposed a memory leak detection method based on bounded model checking for C program called MLD-CBMC. It took C / C ＋＋ program files as input,unwound the program and inserted memory leak properties,encoded the program constraints and properties into verification conditions using satisfiability modulo theory,then passed the verification conditions to a SMT solver. Thus it converted detecting memory leaks to solving satisfiability problems. By experiment and cooperation with other bounded model checking tools,MLD-CBMC shows its feasibility and effectiveness.

关 键 词：C/C++程序 内存泄露 有界模型检测 可满足性模理论 

分 类 号：TP311.53[自动化与计算机技术—计算机软件与理论]