cpachecker
1.0.0
より多くのドキュメントはdoc/ディレクトリにあります。
Cpacheckerは、Apache 2.0ライセンスに基づいて、Dirk Beyerなどによる著作権でライセンスされています（すべての貢献者の完全なリストについてはauthors.mdを参照）。サードパーティライブラリは、他のさまざまなライセンスおよび著作権の下にあります。フルライセンステキストのディレクトリLICENSESのファイル。特に、Mathsatは研究および評価の目的でのみ利用できます（ LICENSES/LicenseRef-MathSAT-CPAchecker.txtを参照）、必要に応じて別のSMTソルバーを使用してください。 GPLプログラムはcpacheckerとともに配布されていますが、Cpacheckerはそのプログラムとは別に、したがってGPLの条件ではないことに注意してください。
すべてのプログラムは、c pre-processorで事前処理する必要があります。つまり、 #defineおよび#includeディレクティブを含めることはできません。コマンドラインで--preprocess指定することにより、Cpachecker内の前処理を有効にできます。複数のCファイルを指定でき、単一のプログラム（実験機能）としてリンクされ、検証されます。
Cpacheckerは、（GNU）cの大きなサブセットを解析して分析することができます。プログラムの解析が失敗した場合は、[email protected]にレポートを送信してください。
確認するソースコードファイルを選択してください。独自のプログラムを使用している場合は、前述のように前処理することを忘れないでください。例： doc/examples/example.cまたはdoc/examples/example_bug.cより多くのプログラムのための優れたソースは、たとえばソフトウェア検証に関する国際競争で使用されるSVベンチマークリポジトリです。
オプション：述語分析などの特定の分析を選択する場合は、構成ファイルを指定します。このファイルは、たとえばどのCPAが使用されるかを定義します。標準構成ファイルは、ディレクトリconfig/にあります。特定の分析が必要ない場合は、CPacheckerのデフォルト構成をお勧めします。ただし、MACOSにいる場合は、デフォルトの構成が機能するために特別にコンパイルされたMathsatバイナリを提供する必要があることに注意してください（または、LinuxバージョンのCPacheckerを実行するためにDockerを使用してください）。 cpacheckerの構成は、 doc/Configuration.mdで説明されています。
仕様ファイルを選択します（一部の構成にはこれは必要ありません）。標準構成では、デフォルトの仕様として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 。たとえばbin/cpachecker --config/kInduction.properties doc/examples/example.cまたは同等の略語bin/cpachecker --kInduction doc/examples/example.cを使用して、特定の分析（k誘導など）を選択できます。 Java 17以降が必要です。パスにない場合は、環境変数Javaで指定する必要があります。例： export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java 。
このプラットフォームにSMTソルバー向けにバイナリを出荷しないため、すべての分析構成がMACOで利用できるわけではないことに注意してください。自分で適切なバイナリを構築するか、Javaベースのソルバーで動作するより強力な分析を使用する必要があります。たとえば、CPacheckerのデフォルト構成ではなく--predicateAnalysis-linear --option solver.solver=SMTInterpolこれは次のとおりです。
dockerを使用してcpacheckerをインストールした場合、上記の例コマンドラインは次のようになります： docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c cpachecker。 CPacheckerの出力ファイルは./output/に配置されます。
コンソール出力に加えて、インタラクティブなHTMLレポートは、 Report.html （結果真の場合）またはCounterexample.*.htmlのいずれかで、ディレクトリoutput/で生成されます。ブラウザでこれらのファイルを開き、cpachecker分析結果を表示します（ doc/Report.mdを参照）
ディレクトリoutput/ ：
ARG.dot ：抽象的な到達可能性ツリーの視覚化（graphviz形式）cfa*.dot ：コントロールフローオートマトンの視覚化（GraphViz形式）reached.dot ：抽象状態が上部で視覚化されたコントロールフローオートマトンの視覚化（GraphViz形式）coverage.info形式のカバレッジ情報（ Gcovツールと同様）は、次のコマンドラインを使用して、 output/index.htmlとして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はこのディレクトリでファイルを上書きします！
CPacheckerの一部であるCPA-Witness2Testで違反証人を検証できます。
そのためには、違反証人、違反証人に適合する仕様ファイル、および違反証人に適合するソースコードファイルが必要です。
証人を検証するには、次のコマンドを実行します。
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.
