cpachecker

Erste Schritte mit CPACHECKER

• Installationsanweisungen
• Beitragsrichtlinien
• Entwicklungsanweisungen

Weitere Dokumentationen finden Sie im doc/ Verzeichnis.

Lizenz und Urheberrecht

CPACHECKER ist unter der Apache 2.0 -Lizenz mit dem Urheberrecht von Dirk Beyer und anderen lizenziert (vgl. Autoren.md für die vollständige Liste aller Mitwirkenden). Bibliotheken von Drittanbietern stehen unter verschiedenen anderen Lizenzen und Urheberrechten, vgl. Die Dateien in den LICENSES für die vollständigen Lizenztexte. Insbesondere ist Mathsat nur für Forschungs- und Bewertungszwecke verfügbar (vgl. LICENSES/LicenseRef-MathSAT-CPAchecker.txt ). Verwenden Sie daher bei Bedarf einen anderen SMT-Solver. Beachten Sie, dass CPACHECKER, obwohl ein GPL -Programm zusammen mit CPachecker verteilt ist, von diesem Programm getrennt ist und somit nicht unter den Bedingungen der GPL ist.

Erstellen Sie Programme zur Überprüfung durch CPACHECKER

Alle Programme müssen mit dem C-Pre-Processor vorverarbeitet werden, dh sie enthalten möglicherweise nicht #define und #include -Richtlinien. Sie können die Vorverarbeitung innerhalb von CPacheCher aktivieren, indem Sie angeben --preprocess in der Befehlszeile. Mehrere C -Dateien können miteinander verknüpft und als einzelnes Programm (experimentelle Funktion) verknüpft und verifiziert werden.

CPACHECKER kann eine große Teilmenge von (GNU) c analysieren und analysieren. Wenn das Parsen für Ihr Programm fehlschlägt, senden Sie bitte einen Bericht an [email protected].

Überprüfen Sie ein Programm mit CPacheCerer

1. Wählen Sie eine Quellcodedatei, die Sie überprüfen möchten. Wenn Sie Ihr eigenes Programm verwenden, denken Sie daran, es wie oben erwähnt vorzuarbeiten. Beispiel: doc/examples/example.c oder doc/examples/example_bug.c Eine gute Quelle für weitere Beispielprogramme ist das SV-Benchmarks-Repository, das beispielsweise vom internationalen Wettbewerb zur Softwareverifizierung verwendet wird.

2. Optional: Wenn Sie bestimmte Analysen wie die Prädikatanalyse auswählen möchten, geben Sie eine Konfigurationsdatei an. Diese Datei definiert beispielsweise, welche CPAs verwendet werden. Standardkonfigurationsdateien finden Sie im Verzeichnis config/ . Wenn Sie keine spezifische Analyse wünschen, empfehlen wir die Standardkonfiguration von CPACHECKER. Beachten Sie jedoch, dass Sie, wenn Sie in MacOS sind, speziell kompilierte Mathsat-Binärdateien für die Standardkonfiguration zur Arbeit bereitstellen müssen (oder Docker verwenden, um die Linux-Version von CPACHECKER auszuführen). Die Konfiguration von CPACHECKER wird in doc/Configuration.md erläutert.

3. Wählen Sie eine Spezifikationsdatei (Sie benötigen dies möglicherweise nicht für einige Konfigurationen). Die Standardkonfigurationen verwenden config/specification/default.spc als Standardspezifikation. In diesem Fall sucht CPACHECKER nach Bezeichnungen mit dem Namen ERROR (Case Inemsibel) und Behauptungen in der Quellcode -Datei. Weitere Beispiele für Spezifikationen finden Sie in config/specification/ im CPACHECKER -Verzeichnis.

4. Führen Sie bin/cpachecker [ --config <CONFIG_FILE> ] [ --spec <SPEC_FILE> ] <SOURCE_FILE> Zusätzliche Befehlszeilenargumente in doc/Configuration.md aus. Um die Standardkonfiguration von CPachecker zu verwenden, übergeben Sie nur die Quelldatei: bin/cpachecker doc/examples/example.c . Eine spezifische Analyse (wie K-Induktion) kann beispielsweise mit bin/cpachecker --config/kInduction.properties doc/examples/example.c oder der äquivalenten Abkürzung bin/cpachecker --kInduction doc/examples/example.c ausgewählt werden. Java 17 oder später ist notwendig. Wenn es nicht auf Ihrem Weg ist, müssen Sie es in der Umgebungsvariablen -Java angeben. Beispiel: export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java für 64bit openjdk 17 auf Ubuntu.

   Bitte beachten Sie, dass nicht alle Analysekonfigurationen für macOS verfügbar sind, da wir keine Binärdateien für SMT -Solver für diese Plattform versenden. Sie müssen entweder die entsprechenden Binärdateien selbst erstellen oder weniger leistungsstarke Analysen verwenden, die mit Java-basierten Solvers arbeiten, beispielsweise diese anstelle der Standardkonfiguration von CPachecker: --predicateAnalysis-linear --option solver.solver=SMTInterpol

   Wenn Sie CPachecker mit Docker installiert haben, würde die obige Beispielbefehlszeile so aussehen: docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c CPACHECKER. Die Ausgabedateien von CPACHECKER werden in ./output/ platziert.

5. Zusätzlich zum Konsolenausgang wird ein interaktives HTML -Bericht im output/ entweder mit dem benannten Report.html (für Ergebnis True) oder Counterexample.*.html (für Ergebnis False). Öffnen Sie diese Dateien in einem Browser, um das Ergebnis der CPachecker -Analyse anzuzeigen (vgl. doc/Report.md ).

Es gibt auch zusätzliche Ausgabedateien in der output/ :

• ARG.dot : Visualisierung der abstrakten Erreichbarkeitsbaum (Graphviz -Format)
• cfa*.dot : Visualisierung des Kontrollflussautomatons (Graphviz -Format)
• reached.dot .
• coverage.info : Abdeckungsinformationen (ähnlich wie bei Testtools) im Gcov Format verwenden die folgende Befehlszeile, um einen HTML-Bericht als output/index.html zu generieren: genhtml output/coverage.info --output-directory output --legend
• Counterexample.*.txt : Ein Pfad durch das Programm, der zu einem Fehler führt
• Counterexample.*.assignment.txt : Zuweisungen für alle Variablen auf dem Fehlerpfad.
• Counterexample.*.harness.c : Ein Testkabelbaum, der den Fehlerpfad durch Testausführung reproduzieren kann. Eine Beispiel Verwendung finden Sie in DOC/Tutorials/Test-HARDES.MD.
• predmap.txt : Prädikate, die durch Prädikatanalyse verwendet werden, um die Programmsicherheit zu beweisen
• reached.txt : Dump aller erreichten abstrakten Zustände
• Statistics.txt : Zeitstatistik (kann auch mit --stats in Konsole gedruckt werden)

Beachten Sie, dass nicht alle diese Dateien für alle Konfigurationen verfügbar sind. Einige dieser Dateien werden auch nur dann erstellt, wenn ein Fehler gefunden wird (oder umgekehrt). CPACHECKER wird Dateien in diesem Verzeichnis überschreiben!

Validierung eines Programms mit CPA-Witness2Test

Sie können Verstoßzeugen mit CPA-Witness2Test validieren, das Teil von CPachecker ist.

1. Zu diesem Zweck benötigen Sie einen Verstöße, eine Spezifikationsdatei, die zum Zeugen von Verstößen entspricht, und die Quellcode -Datei, die zum Verstößerungszeugen entspricht.

2. Um den Zeugen zu validieren, führen Sie den folgenden Befehl aus:

    bin/cpa-witness2test --witness <WITNESS_FILE> --spec <SPEC_FILE> <SOURCE_FILE>`
   

   Addtionale Befehlszeilenargumente werden mit bin/cpa-witness2test -h angesehen.

3. Nach Abschluss und wenn der Zeugen des Verstoßes erfolgreich validiert wird, zeigt die Konsolenausgabe Verification result: FALSE . Zusätzlich zur Konsolenausgabe erstellt CPA-Witness2Test auch eine output/*.harness.c . Diese Datei kann mit der Quelldatei kompiliert werden, um einen ausführbaren Test zu erstellen, der den Verstößerungszeugen widerspiegelt.

Beachten Sie, dass das Validierungsergebnis ERROR ist und die Konsolenausgabe die folgende Zeile enthält, wenn der Zeuge des Verstoßes nicht genügend Informationen enthält, um einen ausführbaren Test zu erstellen: Could not export a test harness, some test-vector values are missing.