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

C/C＋＋语言中的动态内存管理机制自由且灵活,但动态内存的使用容易引入内存泄露,导致系统性能降低甚至系统崩溃。为了更加有效地检测内存泄露,提出了一个基于有界模型检测技术的C/C＋＋程序内存泄露检测方案MLD-CBMC。该方案以C/C＋＋程序文件为输入,利用有界模型检测技术对程序进行展开处理,加入内存泄露性质,并利用可满足性模理论（SMT）对程序约束和性质组成的验证条件编码,使用SMT求解器对验证条件求解,将检测内存泄露问题转换为求解可满足性问题,实现C/C＋＋程序内存泄露的检测。通过实验验证了方案的有效性,并与其他有界模型检测工具进行对比实验,实验证明方案对内存泄露的检测能力更强。