C程序分析工具中程序切片的设计与实现

摘要 符号执行技术以其良好的精确度控制被广泛应用于程序分析领域,它将程序中变量的值用抽象的符号表示,模拟真实的程序执行.由于其路径敏感,在分析过程中会带来严重的状态爆炸问题.提出针对缺陷的程序切片方法来缓解这一问题,首先根据用户关心的缺陷生成源程序的切片准则,然后分析源代码生成数据依赖图和控制依赖图,由两者构成程序依赖图,再根据切片准则做程序切片,将源程序规模缩小,最后将切片后的程序交给程序分析工具分析.在符号执行分析工具ShapeChecker上的实验结果表明,提出的方法具有良好的效果