Installation Instructions: INSTALL.md Develop and Contribute: doc/Developing.md
安装说明：INSTALL.md Develop 和 Contribute：doc/Developing.md

More documentation can be found in the doc folder.
更多文档可以在 doc 文件夹中找到。

CPAchecker is licensed under the Apache 2.0 License with copyright by Dirk Beyer and others (cf. Authors.md for full list of all contributors). Third-party libraries are under various other licenses and copyrights, cf. lib/java-runtime-licenses.txt for an overview and the files in the directory LICENSES for the full license texts. In particular, MathSAT is available for research and evaluation purposes only (cf. LICENSES/LicenseRef-MathSAT-CPAchecker.txt), so make sure to use a different SMT solver if necessary. Note that although a GPL program is distributed together with CPAchecker, CPAchecker is separate from that program and thus not under the terms of the GPL.
CPAchecker 根据 Apache 2.0 许可证获得许可，版权归 Dirk Beyer 和其他人所有（参见 Authors.md 以获取所有贡献者的完整列表）。第三方库受各种其他许可证和版权保护，参见 lib/java-runtime-licenses.txt 了解概述，参见目录 LICENSES 中的文件了解完整的许可证文本。特别是，MathSAT 仅用于研究和评估目的 （cf. LICENSES/LicenseRef-MathSAT-CPAchecker.txt ），因此如有必要，请确保使用不同的 SMT 求解器。请注意，尽管 GPL 程序与 CPAchecker 一起分发，但 CPAchecker 与该程序是分开的，因此不受 GPL 条款的约束。

All programs need to pre-processed with the C pre-processor, i.e., they may not contain #define and #include directives. You can enable pre-processing inside CPAchecker by specifying -preprocess on the command line. Multiple C files can be given and will be linked together and verified as a single program (experimental feature).
所有程序都需要使用 C 预处理器进行预处理，即它们不能包含 #define 和 #include 指令。您可以通过在命令行上指定 -preprocess 在 CPAchecker 中启用预处理。可以给出多个 C 文件，并将链接在一起并作为单个程序进行验证（实验性功能）。

CPAchecker is able to parse and analyze a large subset of (GNU)C. If parsing fails for your program, please send a report to cpachecker-users@googlegroups.com.
CPAchecker 能够解析和分析 （GNU）C 的一大块。如果您的程序解析失败，请向 cpachecker-users@googlegroups.com 发送报告。

1. Choose a source code file that you want to be checked. If you use your own program, remember to pre-process it as mentioned above. Example: doc/examples/example.c or doc/examples/example_bug.c A good source for more example programs is the benchmark set of the International Competition on Software Verification, which can be checked out from https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.
   选择要选中的源代码文件。如果您使用自己的程序，请记住如上所述对其进行预处理。示例：doc/examples/example.c 或 doc/examples/example_bug.c 更多示例程序的一个很好的来源是国际软件验证竞赛的基准集，可以从 https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks 中查看。

2. If you want to enable certain analyses like predicate analysis, choose a configuration file. This file defines for example which CPAs are used. Standard configuration files can be found in the directory config/. If you do not want a specific analysis, we recommend config/default.properties. However, note that if you are on MacOS you need to provide specifically-compiled MathSAT binaries for this configuration to work (or use Docker in order to run the Linux version of CPAchecker). The configuration of CPAchecker is explained in doc/Configuration.md.
   如果要启用某些分析（如谓词分析），请选择一个配置文件。例如，此文件定义使用哪些 CPA。标准配置文件可以在 config/ 目录下找到。如果您不需要特定的分析，我们建议使用 config/default.properties。但是，请注意，如果您使用的是 MacOS，则需要提供专门编译的 MathSAT 二进制文件才能使此配置正常工作（或使用 Docker 来运行 Linux 版本的 CPAchecker）。CPAchecker 的配置在 doc/Configuration.md 中进行了说明。

3. Choose a specification file (you may not need this for some CPAs). The standard configuration files use config/specification/default.spc as the default specification. With this one, CPAchecker will look for labels named ERROR (case insensitive) and assertions in the source code file. Other examples for specifications can be found in config/specification/
   选择一个规范文件（某些 CPA 可能不需要此文件）。标准配置文件用作 config/specification/default.spc 默认规范。有了这个，CPAchecker 将在源代码文件中查找名为 ERROR（不区分大小写）的标签和断言。规范的其他示例可以在 config/specification/ 中找到。

4. Execute scripts/cpa.sh [ -config <CONFIG_FILE> ] [ -spec <SPEC_FILE> ] <SOURCE_FILE> Either a configuration file or a specification file needs to be given. The current directory should be the CPAchecker project directory. Additional command line switches are described in doc/Configuration.md. Example: scripts/cpa.sh -config config/default.properties doc/examples/example.c This example can also be abbreviated to: scripts/cpa.sh -default doc/examples/example.c Java 17 or later is necessary. If it is not in your PATH, you need to specify it in the environment variable JAVA. Example: export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java for 64bit OpenJDK 17 on Ubuntu. On Windows (without Cygwin or WSL), you need to use cpa.bat instead of cpa.sh.
   执行 scripts/cpa.sh [ -config <CONFIG_FILE> ] [ -spec <SPEC_FILE> ] <SOURCE_FILE> 需要提供配置文件或规范文件。当前目录应为 CPAchecker 项目目录。doc/Configuration.md 中介绍了其他命令行开关。示例： scripts/cpa.sh -config config/default.properties doc/examples/example.c 此示例也可以缩写为： scripts/cpa.sh -default doc/examples/example.c Java 17 或更高版本是必需的。如果它不在您的 PATH 中，则需要在环境变量 JAVA 中指定它。示例： export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java 适用于 Ubuntu 上的 64 位 OpenJDK 17。在 Windows（没有 Cygwin 或 WSL）上，您需要使用 cpa.bat 而不是 cpa.sh。

   Please note that not all analysis configurations are available for MacOS because we do not ship binaries for SMT solvers for this platform. You either need to build the appropriate binaries yourself or use less powerful analyses that work with Java-based solvers, for example this one instead of -default: -predicateAnalysis-linear -setprop solver.solver=SMTInterpol Of course you can also use solutions like Docker for executing the Linux version of CPAchecker.
   请注意，并非所有分析配置都可用于 MacOS，因为我们不为此平台提供 SMT 求解器的二进制文件。您要么需要自己构建适当的二进制文件，要么使用与基于 Java 的求解器一起使用的功能较弱的分析，例如这个而不是 -default： -predicateAnalysis-linear -setprop solver.solver=SMTInterpol 当然，您也可以使用 Docker 等解决方案来执行 Linux 版本的 CPAchecker。

   If you installed CPAchecker using Docker, the above example command line would look like this: docker run -v $(pwd):/workdir -u $UID:$GID registry.gitlab.com/sosy-lab/software/cpachecker -default /cpachecker/doc/examples/example.c This command makes the current directory available in the container, so to verify a program in the current directory just provide its file name instead of the example that is bundled with CPAchecker. Output files of CPAchecker will be placed in ./output/.
   如果您使用 Docker 安装了 CPAchecker，则上面的示例命令行将如下所示： docker run -v $(pwd):/workdir -u $UID:$GID registry.gitlab.com/sosy-lab/software/cpachecker -default /cpachecker/doc/examples/example.c 此命令使当前目录在容器中可用，因此要验证当前目录中的程序，只需提供其文件名，而不是与 CPAchecker 捆绑在一起的示例。CPAchecker 的输出文件将放置在 ./output/ 中。

5. Additionally to the console output, an interactive HTML report is generated in the directory output/, either named Report.html (for result TRUE) or Counterexample.*.html (for result FALSE). Open these files in a browser to view the CPAchecker analysis result (cf. doc/Report.md)
   除了控制台输出之外，还会在目录 output/ 中生成一个交互式 HTML 报告，名称为 Report.html（对于结果 TRUE）或 Counterexample.*.html（对于结果 FALSE）。在浏览器中打开这些文件以查看 CPAchecker 分析结果（参见 doc/Report.md）

There are also additional output files in the directory output/:
目录 output/ 中还有其他输出文件：

• ARG.dot: Visualization of abstract reachability tree (Graphviz format)
  ARG.dot：抽象可达性树的可视化（Graphviz 格式）
• cfa*.dot: Visualization of control flow automaton (Graphviz format)
  cfa*.dot：控制流自动机的可视化（Graphviz 格式）
• reached.dot: Visualization of control flow automaton with the abstract states visualized on top (Graphviz format)
  reached.dot：控制流自动机的可视化，抽象状态可视化在顶部（Graphviz 格式）
• coverage.info: Coverage information (similar to those of testing tools) in Gcov format Use the following command line to generate an HTML report as output/index.html: genhtml output/coverage.info --output-directory output --legend
coverage.info：Gcov 格式的覆盖率信息（类似于测试工具的信息）使用以下命令行生成 HTML 报告 output/index.html： genhtml output/coverage.info --output-directory output --legend
• Counterexample.*.txt: A path through the program that leads to an error
• Counterexample.*.assignment.txt: Assignments for all variables on the error path.
• predmap.txt: Predicates used by predicate analysis to prove program safety
• reached.txt: Dump of all reached abstract states
• Statistics.txt: Time statistics (can also be printed to console with -stats)

Note that not all of these files will be available for all configurations. Also some of these files are only produced if an error is found (or vice-versa). CPAchecker will overwrite files in this directory!

You can validate violation witnesses with CPA-witness2test, which is part of CPAchecker.

1. To do so, you need a violation witness, a specification file that fits the violation witness, and the source code file that fits the violation witness.

2. To validate the witness, execute the following command:

   scripts/cpa_witness2test.py -witness <WITNESS_FILE> -spec <SPEC_FILE> <SOURCE_FILE>`
   

   Addtional command line switches are viewed with scripts/cpa_witness2test.py -h.

3. When finished, and if the violation witness is successfully validated, the console output shows Verification result: FALSE. Additionally to the console output, CPA-witness2test also creates a file output/*.harness.c. This file can be compiled against the source file to create an executable test that reflects the violation witness.

Note that if the violation witness does not contain enough information to create an executable test, the validation result will be ERROR and the console output will contain the following line: Could not export a test harness, some test-vector values are missing.