文章预览
引子 前一篇文章介绍了堆栈和内存的一些背景知识。本次介绍如何使用 Polyspace Code Prover来统计堆栈,如何使用这些数据为软件优化服务。 👉前文:堆栈统计知多少(一)关于内存,堆栈和常见的 BUG ▼ Polyspace Code Prover 堆栈统计 前面三类堆栈统计工具,在统计堆栈使用的时候,其需要编译并运行代码,这意味着其需要定义测试激励,这种情况的堆栈统计是特定测试激励的,其他时候的堆栈大小则需要定义合适的测试激励。而要统计软件的最大堆栈需求,则需要设计合适的测试用例。这无疑对测试用例有比较高的要求。 形式化工具 Polyspace Code Prover 使用抽象解释法,能够深入探测到每一层函数的调用,统计每个函数本身的局部变量消耗和因为函数调用需要的栈消耗。另外,由于形式化的方法的使用,Polyspace Code Prover 能够分析代码中的分支是否因为
………………………………