cbmc:C绑定模型检查器 源码

关于 CBMC是用于C和C ++程序的绑定模型检查器。 它支持C89,C99,大多数C11和gcc和Visual Studio提供的大多数编译器扩展。 它还使用Scoot支持SystemC。 它允许验证数组边界(缓冲区溢出),指针安全性,异常和用户指定的断言。 此外,它可以检查C和C ++与其他语言(例如Verilog)的一致性。 通过展开程序中的循环并将结果方程式传递到决策程序来执行验证。 有关完整信息,请访问 。 有关CProver包含的各种工具以及如何使用它们的概述,请参见 。 版本号 获取 版本已经过测试,可用于生产。 获取当前的开发版本: git clone https://github.com/diffblue/cbmc.git 不建议将开发版本用于生产。 正在安装 视窗 对于Windows,您可以通过页面上的.msi安装cbmc二进制文件。 请注意,我们依赖于Vis