Frama-C ist eine Open-Source-Plattform zur Analyse von C-Quellcode; sie bündelt mehrere Analysetechniken in einem gemeinsamen Rahmenwerk. Die formale Spezifikationssprache heißt ACSL (ANSI/ISO C Specification Language), ausgewählte Plug-ins führen statische Analyse und Verifikation durch.
Aufruf von der Kommandozeile
frama-c -eva datei.c # abstrakte Interpretation (Werte)
frama-c -wp datei.c # Schwaechste-Vorbedingung, Beweis
frama-c -wp -wp-prover alt-ergo datei.c
frama-c -metrics datei.c # Metriken
frama-c -gui datei.c # graphische Oberflaeche (frama-c-gui)Das EVA-Plug-in (ab 18.0; vorher VALUE) überapproximiert die möglichen Werte von Variablen an jedem Programmpunkt und findet so Laufzeitfehler wie Überläufe oder Zugriffe außerhalb von Feldgrenzen. Das WP-Plug-in implementiert einen Weakest-Precondition-Kalkül und erzeugt Verifikationsbedingungen (VCs), die an externe Beweiser wie Alt-Ergo, Z3 oder CVC4 gehen.
ACSL-Annotationen
/*@ requires 0 <= n && n < 100;
@ ensures
esult == n * n;
@*/
int quadrat(int n) { return n * n; }requires: Vorbedingung,ensures: Nachbedingung,assigns: erlaubte Seiteneffekte.//@ assert p;: lokale Behauptung,//@ loop invariant: Schleifeninvariante.esult,old(expr),valid(p),separated(...): Terme für Rückgabe, Alt-Werte, Zeiger-Gültigkeit.
Frama-C ergänzt die Beweisassistenten-Familie um eine C-spezifische, praktische Verifikation: verwandt sind VDM, PVS und SPIN/Promela; als C-Anker dient C/C++-Befehle.