cpachecker
1.0.0
可以在doc/目录中找到更多文档。
CPACHECKER由Dirk Beyer等人获得Apache 2.0许可证的许可（参见Author.md，用于所有贡献者的完整列表）。第三方图书馆属于其他各种许可和版权，参见。完整许可文本目录LICENSES中的文件。特别是，MathSat仅用于研究和评估目的（参见LICENSES/LicenseRef-MathSAT-CPAchecker.txt ），因此请确保在必要时使用其他SMT求解器。请注意，尽管GPL程序与Cpachecker一起分发，但Cpachecker与该程序分开，因此不在GPL的条款下。
所有程序都需要与C前处理器进行预处理，即，它们可能不包含#define和#include指令。您可以通过在命令行上指定cpachecker内部进行--preprocess 。可以给出多个C文件，并将链接在一起并验证为单个程序（实验功能）。
Cpachecker能够解析和分析（GNU）c的大部分子集。如果您的程序解析失败，请向[email protected]发送报告。
选择要检查的源代码文件。如果您使用自己的程序，请记住如上所述对其进行预处理。示例： doc/examples/example.c或doc/examples/example_bug.c更多示例程序的良好来源是SV-Benchmarks存储库，例如国际竞赛在软件验证方面使用的源。
选项：如果要选择某些分析（例如谓词分析），请指定配置文件。该文件定义了使用哪些CPA。标准配置文件可以在目录config/中找到。如果您不需要特定的分析，我们建议使用CPACHECKER的默认配置。但是，请注意，如果您在MacOS上，则需要提供专门编译的Mathsat二进制文件以使默认配置工作（或使用Docker来运行Cpachecker的Linux版本）。 doc/Configuration.md中解释了cpachecker的配置。
选择一个规范文件（您可能不需要某些配置）。标准配置使用config/specification/default.spc作为默认规范。有了这一点，Cpachecker将在源代码文件中寻找名为ERROR （情况不敏感）和断言的标签。其他规格的示例可以在config/specification/ cpachecker目录中找到。
执行bin/cpachecker [ --config <CONFIG_FILE> ] [ --spec <SPEC_FILE> ] <SOURCE_FILE>其他命令行参数在doc/Configuration.md中描述。要使用CPACHECKER的默认配置，请仅通过源文件： bin/cpachecker doc/examples/example.c 。可以选择特定的分析（例如k诱导），例如使用bin/cpachecker --config/kInduction.properties doc/examples/example.c或等效的缩写bin/cpachecker --kInduction doc/examples/example.c 。 Java 17或以后是必要的。如果不在您的路径中，则需要在环境变量Java中指定它。示例： export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java for Ubuntu上的64bit OpenJdk 17。
请注意，并非所有分析配置都用于MACOS，因为我们没有为此平台运送SMT求解器的二进制文件。您要么需要自己构建适当的二进制文件，要么使用与基于Java的求解器一起使用的功能较低的分析，例如，它而不是Cpachecker的默认配置： --predicateAnalysis-linear --option solver.solver=SMTInterpol当然您还可以使用Docker等解决方案来执行CPACHECKERDER Linux版本。
如果您使用Docker安装了CPACHECKER，则上述示例命令行看起来像： docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c此命令在informentife中提供了当前命令，因此可以验证该命名的名称，以验证该命名的名称，以替代程序，以替代程序，以替代程序，以供名方提供。 CPACHECKER。 Cpachecker的输出文件将放置在./output/中。
除了控制台输出外，在目录output/命名Report.html （为true）或Counterexample.*.html中生成了交互式HTML报告。在浏览器中打开这些文件以查看CPACHECKER分析结果（参见doc/Report.md ）
目录output/ ：：
ARG.dot ：抽象可达性树的可视化（GraphViz格式）cfa*.dot ：控制流动自动机的可视化（GraphViz格式）reached.dot 。coverage.info Gcov中的覆盖信息（类似于测试工具的覆盖范围信息（类似于测试工具的工具）使用以下命令行来生成HTML报告作为output/index.html genhtml output/coverage.info --output-directory output --legendCounterexample.*.txt ：导致错误的程序的路径Counterexample.*.assignment.txt ：错误路径上所有变量的分配。Counterexample.*.harness.c ：可以通过测试执行重现错误路径的测试安全带。有关示例使用，请参见DOC/TUTORIALS/TEST-HARNESS.MD。predmap.txt ：谓词分析用来证明程序安全性的谓词reached.txt ：所有达到抽象状态的转储Statistics.txt ：时间统计（也可以用--stats打印到控制台）请注意，并非所有这些文件都可以用于所有配置。另外，仅当发现错误（或反之亦然）时，这些文件中的某些文件才会产生。 Cpachecker将在此目录中覆盖文件！
您可以用CPA-Witness2Test验证违规证人，这是Cpachecker的一部分。
为此，您需要违规证人，适合违规证人的规范文件以及适合违规证人的源代码文件。
要验证证人，请执行以下命令：
bin/cpa-witness2test --witness <WITNESS_FILE> --spec <SPEC_FILE> <SOURCE_FILE>`
使用bin/cpa-witness2test -h查看附加命令行参数。
完成后，如果违规证人已成功验证，控制台输出将显示Verification result: FALSE 。除了控制台输出外，CPA-Witness2Test还创建文件output/*.harness.c 。可以针对源文件编译此文件，以创建反映违规证人的可执行测试。
请注意，如果违规证人不包含足够的信息来创建可执行测试，则验证结果将是ERROR ，并且控制台输出将包含以下行： Could not export a test harness, some test-vector values are missing.
