一种可扩展的C代码静态分析方法研究  

作　　者：余亚刚[1] 邱征[1] 魏雪菲[1] 

机构地区：[1]中航工业西安航空计算技术研究所,陕西西安710119

出　　处：《科技风》2012年第14期13-16,共4页

摘　　要：为降低软件工程项目的开发风险和后期维护成本,本文提出一种模型检验的可扩展C代码静态检查方法。该方法将C代码常见错误归纳为可扩展的计算树逻辑公式库,同时将被检测代码转化成为程序控制流图,并将该图抽象为等价的Kripke结构;依据Kripke结构模型,使用NuSMV工具验证公式库中的公式是否满足代码检查的要求;最后采用GCC编译平台提供静态检查的实验结果。该方法可以找到代码中用户事先配置的错误模式,消除代码隐患。

关 键 词：计算树逻辑(CTL) 程序控制流图(CFG) 代码静态分析 错误模式 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]