Vij*_*ali 6 c static-analysis invariants
我正在寻找一种可以在C程序中静态发现不变量的工具.我检查了Daikon,但它只是动态发现不变量.
是否有可用于我正在寻找的工具？谢谢!
如果您指的是最广泛意义上的“不变量”，就像 Daikon 的链接页面所使用的那样，那么许多静态分析工具的工作可以被描述为“发现不变量”，只是可能不是您正在寻找的表达不变量。
\n\nFrama-C 的值分析会累积其结果，即每个语句的所有变量的可能值。在分析结束时，它可以在每个语句处提供有关程序中每个变量的域变化的非关系信息。在此屏幕截图中，对于该确定性程序的所有执行，不变式是S在所选指令之前始终为 0、1、3 或 6。
您问题中的两个隐藏参数是您感兴趣的不变量的形状，以及您想要查找这些不变量的程序的形状。例如，Ira 的回答中提到的 SLAM 旨在处理设备驱动程序代码，并推断仅包含验证系统 API 正确使用所需信息的不变量。另一个工具Asstr\xc3\xa9e因在推断正确的不变量以演示飞行控制软件的运行时安全性方面做得非常出色而闻名。
\n\n这两个自由度构成了非常大的设计空间。您不会找到适用于所有类型的 C 程序并推断您可能感兴趣的所有不变量的任何内容，但如果您针对特定应用程序领域和不变量类型细化您的问题，您将有更好的机会找到相关答案。
\n