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.
