C 有界模型检查器
CBMC 是一个用于 C 和 C++ 程序的有界模型检查器。 它支持 C89、 C99、C11 的大部分、C17、C23 以及由 gcc 提供的大多数编译器扩展 Visual Studio。 它还支持使用 Scoot 的 SystemC。 它允许验证 数组边界 (缓冲区溢出)、指针安全性、异常和 此外,它还可以检查 C 和 C++ 语言中的代码, 与其他语言如 Verilog 保持一致。验证过程是 通过解除程序中的循环并传递所产生的结果来执行 将方程转换为决策过程。 如需完整信息,请参阅 cprover.org。
如需了解 CProver 中的各种工具以及如何使用它们，请参阅 TOOLS_OVERVIEW.md。
对于不同的 Linux 环境,您可以选择以下两种方式:
暂无开放 Issues，或尚未同步最近议题。