Frama C snapshot

Frama-C ist eine Plattform, die der Analyse des in C geschriebenen Quellcodes gewidmet ist

Hinweis: Das offizielle Frama-C-Repository befindet sich jetzt in unserem Gitlab!

Frama-C hat sein offizielles Repository in unsere selbst gehostete Gitlab-Instanz verlegt.

Offizielle Veröffentlichungen (ab Frama-C 21) werden hier nicht mehr aktualisiert.

Nightly Snapshots sind auch in unserem GitLab erhältlich! Sie erhalten jetzt Zugriff auf die neueste Entwicklungsversion unter: https://git.frama-c.com/pub/frama-c/-/tree/master

Der offizielle Frama-C-Ausgabe-Tracker ist jetzt in unserem GitLab: https://git.frama-c.com/pub/frama-c/-/issues

Sie können Probleme mit Ihrem GitHub -Anmeldung einreichen und Anfragen ziehen (wählen Sie bei der Aufforderung mit GitHub an).

Wir sehen uns dort!

Eine kollaborative Plattform

Frama-C versammelt mehrere Analysetechniken in einer einzigen kollaborativen Plattform, die aus einem Kernel besteht, der einen Kernsatz von Funktionen (z. B. ein normalisierter AST für C-Programme) sowie eine Reihe von Analysatoren namens Plug-Ins bietet. Plug-Ins können auf Ergebnissen erstellen, die von anderen Plug-Ins in der Plattform berechnet werden.

Dank dieses Ansatzes bietet Frama-C anspruchsvolle Tools, darunter:

• ein Analysator, der auf abstrakter Interpretation basiert, die darauf abzielte, das Fehlen von Laufzeitfehlern ( EVA ) zu überprüfen;
• ein programmsicheres Framework, das auf dem schwächsten Voraussetzungskalkül ( WP ) basiert;
• ein Programm Slicer ( Schneiden );
• ein Instrument zur Überprüfung der zeitlichen (LTL) Eigenschaften ( aoraï );
• ein Laufzeitüberprüfungswerkzeug ( E-ACSL );
• Mehrere Tools für die Exploration und Abhängigkeit von Codebasis und Abhängigkeit ( von Auswirkungen , Metriken , Auftreten , Umfang usw.).

Diese Plug-Ins teilen eine gemeinsame Sprache und können Informationen über ACSL- Eigenschaften ( ANSI/ISI C-Spezifikationssprachen ) austauschen. Plug-Ins können auch über ihre APIs zusammenarbeiten.

Installation

Weitere Informationen zur Installation von OPAM/Frama-C finden Sie in Install.md.

Frama-C ist über Opam, den OCAML-Paketmanager, erhältlich. Dies ist die bevorzugte Installationsmethode. Stellen Sie sicher, dass Sie OPAM v2.0 oder höher installieren. Dann sollte die folgende Folge von Befehlen Frama-C und seine GUI installieren:

 opam init
opam install depext
opam depext frama-c
opam install frama-c

Frama-C wird hauptsächlich in Linux entwickelt, häufig in macOS (über Homebrew) getestet und gelegentlich unter Windows (über das Windows-Subsystem für Linux) getestet.

Verwendung

Frama-C kann von der Befehlszeile oder über seine grafische Schnittstelle ausgeführt werden.

Einfache Verwendung

Die empfohlene Verwendung für einfache Dateien ist eine der folgenden Zeilen:

 frama-c file.c -<plugin> [options]
frama-c-gui file.c

Wobei -<plugin> eines der verschiedenen Frama -wp -Plug -Ins ist, -metrics -eva

Um alle Plug-Ins aufzulisten, rennen Sie:

 frama-c -plugins

Jedes Plug-In verfügt über einen Hilfebefehl ( -<plugin>-help oder- -<plugin>-h ), der seine verschiedenen Optionen beschreibt.

Schließlich ist die Liste der Optionen, die das Verhalten des Kernels von Frama-C selbst regeln, durch verfügbar

 frama-c -kernel-help

Komplexe Szenarien

Für komplexere Nutzungsszenarien (viele Dateien und Verzeichnisse mit mehreren Vorverarbeitungsrichtlinien) empfehlen wir, die Verwendung von Frama-C in zwei Teilen zu teilen:

1. Analyse der Eingabedateien und Speichern des Ergebnisses in einer Datei;
2. Laden der Parsing -Ergebnisse und dann die Analysen oder die GUI.

Das Parsen beinhaltet in der Regel zusätzliche Argumente an den C-Präprozessor, sodass die Option -cpp-extra-args häufig nützlich ist, wie im folgenden Beispiel:

 frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav

Die Ergebnisse werden dann für weitere Analysen oder zur Inspektion über die GUI in Frama-C geladen:

 frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]

Weitere Referenz

• Links zu Benutzer- und Entwicklerhandbüchern, Frama-C-Archiven und Plug-in-Handbüchern finden Sie unter
  http://frama-c.com/download.html

• Stackoverflow hat mehrere Fragen mit dem frama-c Tag, das von mehreren Mitgliedern der Frama-C-Community überwacht wird.

• Die Frama-C-Discuss-Mailingliste wird für Ankündigungen und allgemeine Diskussionen verwendet.

• Das offizielle Fehlerverfolgungssystem kann für Fehlerberichte verwendet werden.

• Das Frama-C-Wiki hat einige nützliche Informationen, obwohl es nicht ganz auf dem neuesten Stand ist.

• Der Frama-C-Blog verfügt über mehrere Beiträge über neue Entwicklungen von Frama-C sowie allgemeine Diskussionen über die C-Sprache, das undefinierte Verhalten, Schwimmpunktberechnungen usw.

• Das Github Snapshot-Repository enthält das .tar.gz-Archiv stabiler Frama-C-Veröffentlichungen, die bereit sind, kloniert zu werden. Es kann auch zur Meldung von Problemen und zur Übermittlung von Pull -Anfragen verwendet werden.