frama-c-gui – Online in der Cloud

PROGRAMM:

NAME/FUNKTION

frama-c[.byte] – ein statischer Analysator für C-Programme

frama-c-gui[.byte] – die grafische Oberfläche von frama-c

ZUSAMMENFASSUNG

frama-c [ Optionen ] Dateien

BESCHREIBUNG

frama-c ist eine Suite von Tools zur Analyse von in C geschriebenem Quellcode
vereint mehrere statische Analysetechniken in einem einzigen kollaborativen Framework. Das
Das Framework kann durch zusätzliche Plugins erweitert werden, die in der platziert werden $FRAMAC_PLUGIN Verzeichnis.
Der Befehl

frama-c -help

stellt die vollständige Liste der derzeit installierten Plugins bereit.

frama-c-gui ist die grafische Benutzeroberfläche von frama-c. Es bietet die gleichen Optionen wie
die Befehlszeilenversion.

frama-c.byte und frama-c-gui.byte sind die OCAML-Bytecode-Versionen der Befehlszeile und
grafische Benutzeroberfläche bzw.

Standardmäßig erkennt Frama-C .c Dateien als C-Dateien, die vorverarbeitet werden müssen und .i Dateien als
C-Dateien wurden bereits vorverarbeitet. Einige Plugins erweitern möglicherweise die Liste der erkannten Plugins
Dateien. Die Vorverarbeitung kann über angepasst werden -cpp-Befehl und -cpp-extra-args
Optionen.

OPTIONAL

Syntax

Unter das Formular können auch Optionen geschrieben werden, die einen zusätzlichen Parameter annehmen

-zu erhalten=stoppen

Diese Option ist obligatorisch, wenn stoppen beginnt mit einem Bindestrich ('-')

Die meisten Optionen, die keinen Parameter benötigen, verfügen über einen entsprechenden Parameter

-Nein-Möglichkeit

Option, die den gegenteiligen Effekt hat.

Hilfe Optionen

-Hilfe gibt einen kurzen Nutzungshinweis und die Liste der installierten Plugins.

-kernel-help
gibt die Liste der vom Frama-C-Kernel erkannten Optionen aus

-verbose n
Legt den Ausführlichkeitsgrad fest (Standard ist 1). Wenn Sie den Wert auf 0 setzen, wird weniger Fortschritt ausgegeben
Mitteilungen. Dieses Level kann auch pro Person eingestellt werden Plugin Basis, mit Option -Plugin-
ausführlich n. Der Ausführlichkeitsgrad des Kernels kann mit der Option gesteuert werden
-kernel-ausführlich n.

-debuggen n
Legt die Debugging-Ebene fest (Standard ist 0, d. h. keine Debugging-Meldungen). Diese Option
hat die gleichen Spezialisierungen pro Plugin (und Kernel) wie -verbose.

-ruhig Setzt Ausführlichkeit und Debugging-Level auf 0.

Optionen Regelung Frama-Cs Kern

-absolut gültiger Bereich
berücksichtigt alle numerischen Adressen im Bereich Minimal Maximal sind gültig. Grenzen sind
als ocaml-Integer-Konstanten analysiert. Standardmäßig sind alle numerischen Adressen
als ungültig angesehen.

-Pfad hinzufügen p1[,p2[...,pn]]
fügt Verzeichnisse hinzu bis zur Liste der Verzeichnisse, in denen sich Plugins befinden
gesucht

[-no]-allow-duplication
ermöglicht die Duplizierung kleiner Blöcke während der Normalisierung von Tests und Schleifen.
Andernfalls werden bei der Normalisierung Labels und Gotos verwendet. Größere Blöcke und Blöcke mit nicht
trivialer Kontrollfluss wird niemals dupliziert. Der Standardwert ist „Ja“.

[-no]-annot
liest die ACSL-Anmerkung. Dies ist die Standardeinstellung. Anmerkungen werden von nicht vorverarbeitet
Standard. Verwenden -pp-annot dafür.

-big-ints-hex max
ganze Zahlen größer als max werden hexadezimal angezeigt (standardmäßig sind es alle Ganzzahlen).
wird in Dezimalzahl angezeigt)

-prüfen Führt Integritätsprüfungen für den internen AST durch (nur für Entwickler).

[-no]-collapse-call-cast
ermöglicht eine implizite Umwandlung zwischen dem von einer Funktion zurückgegebenen Wert und dem L-Wert, um den es sich handelt
Zugewiesen an. Andernfalls wird eine temporäre Variable verwendet und die Umwandlung explizit gemacht.
Der Standardwert ist „Ja“.

[-no]-constfold
Faltet alle syntaktisch konstanten Ausdrücke im Code vor der Analyse. Standardeinstellungen
zu Nr.

[-no]-continue-annot-error
Beim Analysieren einer Anmerkung wird das Standardverhalten (das -Nein Version dieser Option)
Wenn ein Fehler bei der Typprüfung auftritt, ist die Quelldatei abzulehnen, wie dies der Fall ist
Typprüfungsfehler im C-Code. Wenn diese Option aktiviert ist, wird die Typprüfung ausgeführt
Geben Sie lediglich eine Warnung aus und verwerfen Sie die Anmerkung, die Typprüfung wird jedoch fortgesetzt
(Fehler im C-Code sind jedoch immer noch schwerwiegend).

-cpp-Befehl cmd
Verwendung cmd als Befehl zur Vorverarbeitung von C-Dateien. Standardmäßig ist die CPP Umwelt
variabel oder zu

gcc -C -E -I.

wenn es nicht eingestellt ist. Um ACSL-Annotationen beizubehalten, muss der Präprozessor diese beibehalten
Kommentare (die -C Option für gcc). %1 und %2 kann verwendet werden in cmd um die zu bezeichnen
Originalquelldatei bzw. die vorverarbeitete Datei

-cpp-extra-args args
Gibt dem Präprozessor zusätzliche Argumente. Dies ist nur dann sinnvoll, wenn
-Vorverarbeitung-Anmerkung eingestellt ist. Die Vorverarbeitung von Anmerkungen erfolgt in zwei separaten Vorverarbeitungsschritten.
Verarbeitungsstufen. Der erste ist ein normaler Durchgang des C-Codes, der das Makro beibehält
Definitionen. Diese werden dann im zweiten Durchgang verwendet, in dem Anmerkungen erstellt werden
vorverarbeitet. args werden nur für den ersten Durchgang verwendet, sodass die Argumente das sind
sollte nicht doppelt verwendet werden (z. B. zusätzliche Include-Direktiven oder Makros).
Definitionen) müssen also dorthin gehen -cpp-Befehl.

[-no]-dynlink
Wenn diese Option aktiviert ist, werden alle im Suchpfad gefundenen dynamischen Plug-Ins geladen (siehe -Druck-Plugin-
Weg Weitere Informationen zum Standardsuchpfad finden Sie hier. Ansonsten nur Plugins
angefordert von -Lademodule wird geladen. Das Standardverhalten ist aktiviert.

-Aufzählungen Repr
Wählen Sie die Art und Weise aus, wie die Darstellung von Aufzählungstypen bestimmt wird. frama-c
-Aufzählungen Hilfe gibt die Liste der verfügbaren Optionen an. Standard ist gcc-enums

-Float-Ziffern n
Bei der Ausgabe von Gleitkommazahlen wird angezeigt n Ziffern. Standardmäßig ist 12.

-float-flush-to-null
Gleitkommaoperationen bündig auf Null

-float-hex
Gleitkommazahlen als Hexadezimalzahl anzeigen

-float-normal
Anzeige von Floats mit der Standard-Ocaml-Routine

-float-relativ
Float-Intervall anzeigen als [ Lower_bound++Breite ]

[-no]-force-rl-arg-eval
erzwingt die Auswertungsreihenfolge von rechts nach links für Argumente von Funktionsaufrufen. Ansonsten
Die Auswertungsreihenfolge bleibt wie im C-Standard unbestimmt. Der Standardwert ist „Nein“.

-journal-deaktivieren
Kein Journal der aktuellen Sitzung ausgeben. Sehen -journal-aktivieren.

-journal-aktivieren
Standardmäßig aktiviert, wird ein Protokoll aller während der aktuellen Aktion ausgeführten Aktionen erstellt
Frama-C-Sitzung in Form eines OCAML-Skripts, mit dem abgespielt werden kann -Belastung-
Skript. Der Name des Skripts kann mit festgelegt werden -Tagebuchname .

-Tagebuchname Name
Legen Sie den Namen der Journaldatei fest (ohne .ml Verlängerung). Standardmäßig ist
frama_c_journal.

-initialisierte-padding-locals
Durch die implizite Initialisierung von Locals werden die Füllbits auf 0 gesetzt. Bei „false“ werden die Füllbits gesetzt
bleiben nicht initialisiert (Standardeinstellung ist „Ja“).

[-no]-keep-comments
Versucht, Kommentare beim Pretty-Printing des Quellcodes beizubehalten (Standardeinstellung ist „Nein“).

[-no]-keep-switch
Wann -simplify-cfg gesetzt ist, behält switch-Anweisungen bei. Der Standardwert ist „Nein“.

-keep-unused-specified-functions
See -Entferne-unbenutzte-angegebene-Funktionen

[-no]-lib-Eintrag
Zeigt an, dass der Einstiegspunkt während der Programmausführung aufgerufen wird. Dies impliziert in
Insbesondere kann nicht davon ausgegangen werden, dass globale Variablen ihre Anfangswerte haben.
Die Standardeinstellung ist -no-lib-Eintrag: Der Einstiegspunkt ist auch der Ausgangspunkt des
Programm und Globals haben ihren Anfangswert.

-Belastung Datei
Laden Sie den darin enthaltenen (zuvor gespeicherten) Status Datei.

-Lademodul m1[,m2[...,mn]]
lädt die ocaml-Module bis . Diese Module müssen sein .cmxsDateien für die
Native Code-Version von Frama-c und .Wieor.cmaDateien für die Bytecode-Version (siehe
Weitere Informationen finden Sie im Abschnitt Dynlink des Ocaml-Handbuchs. Alle Module, die sind
Die im Plugin vorhandenen Suchpfade werden automatisch geladen.

-load-script s1[,s2,[...,sn]]
lädt die OCAML-Skripte bis . Die Skripte müssen sein .mlDateien. Sie
muss kompilierbar sein und sich ausschließlich auf die Ocaml-Standardbibliothek und die Frama-C-API verlassen. Wenn
Es ist ein benutzerdefinierter Kompilierungsschritt erforderlich. Kompilieren Sie diese außerhalb von Frama-C und verwenden Sie sie
-Lademodul stattdessen.

-machdep Maschine
verwendet Maschine B. die aktuelle maschinenabhängige Konfiguration (Größe der verschiedenen
Integer-Typen, Endiantness, ...). Die Liste der aktuell unterstützten Maschinen ist
verfügbar durch -machdep Hilfe Möglichkeit. Standard ist x86_32

-Main f
Sets f als Einstiegspunkt der Analyse. Der Standardwert ist „main“. Standardmäßig ist dies der Fall
als Ausgangspunkt des zu analysierenden Programms betrachtet. Verwenden -lib-Eintrag if f
soll mitten in einer Hinrichtung aufgerufen werden.

-verwirren
gibt eine verschleierte Version des Codes aus (wobei die ursprünglichen Bezeichner ersetzt werden).
durch bedeutungsloses) und beendet. Die Entsprechungstabelle zwischen Original und Neu
Symbole werden am Anfang des Ergebnisses beibehalten.

-ocode Datei
leitet hübsch gedruckten Code um Datei statt Standardausgabe.

[-no]-orig-name
Während der Normalisierungsphase werden einige Variablen möglicherweise umbenannt, wenn sie sich unterscheiden
Variable mit demselben Namen können nebeneinander existieren (z. B. eine globale Variable und eine formale Variable).
Parameter). Wenn diese Option aktiviert ist, wird jedes Mal eine Meldung gedruckt, wenn dies geschieht.
Standardmäßig auf Nr.

[-no]-warn-signed-downcast
Generieren Sie Alarme, wenn signierte Downcasts den Zielbereich überschreiten könnten (Standardeinstellung).
nicht).

[-no]-warn-signed-overflow
Generieren Sie Alarme für signierte Vorgänge, die überlaufen (Standardeinstellung ist „Ja“).

[-no]-warn-unsigned-downcast
Generieren Sie Alarme, wenn nicht signierte Downcasts den Zielbereich überschreiten könnten (Standard).
zu nein).

[-no]-warn-unsigned-overflow
Generieren Sie Alarme für nicht signierte Vorgänge, die überlaufen (Standardeinstellung: Nein).

[-no]-pp-annot
Anmerkungen vor dem Prozess. Dies ist derzeit nur bei Verwendung von gcc (oder GNU) möglich
cpp) Präprozessor. Standardmäßig werden Anmerkungen nicht vorverarbeitet.

[-no]-print
Druckt den Quellcode hübsch aus, wie er von CIL normalisiert wird (standardmäßig „no“).

-print-libpath
gibt das Verzeichnis aus, in dem die Frama-C-Kernelbibliothek installiert ist

-Druckpfad
Alias ​​von -print-share-path

-Plugin-Pfad drucken
gibt das Verzeichnis aus, in dem Frama-C seine Plugins durchsucht (kann durch überschrieben werden
FRAMAC_PLUGIN Variable und die -Pfad hinzufügen Option)

-print-share-path
gibt das Verzeichnis aus, in dem Frama-C seine Daten speichert (kann durch überschrieben werden).
FRAMAC_SHARE Variable)

-Entferne-unbenutzte-angegebene-Funktionen
Behält Funktionsprototypen, die eine ACSL-Spezifikation haben, aber nicht im verwendet werden
Code. Dies ist die Standardeinstellung. Funktionen mit dem Attribut FRAMAC_BUILTIN sind immer
gehalten.

-sichere-Arrays
Bei mehrdimensionalen Arrays oder Arrays, die Felder innerhalb von structs sind, wird davon ausgegangen
Alle Zugriffe müssen in gebundener Form erfolgen (standardmäßig festgelegt). Die entgegengesetzte Option ist -unsicher-
Arrays

-speichern Datei
Speichert den Zustand von Frama-C Datei nachdem Analysen stattgefunden haben.

[-no]-simplify-cfg
Entfernt die Anweisungen break, continue und switch vor der Analyse. Der Standardwert ist „Nein“.

-dann Ermöglicht das Verfassen von Analysen: Es erfolgt ein erster Durchlauf von Frama-C mit den Optionen
Bevor -dann und ein zweiter Durchlauf wird mit den folgenden Optionen durchgeführt -dann auf die
aktuelles Projekt aus dem ersten Durchlauf.

-dann-auf prj
Ähnlich -dann außer dass der zweite Lauf im Projekt durchgeführt wird prj Wenn keine solche
Wenn das Projekt vorhanden ist, wird Frama-C mit einem Fehler beendet.

-Zeit Datei
Hängt Benutzerzeit und -datum an die angegebene Stelle an Datei wenn Frama-C aussteigt.

-Typenprüfung
erzwingt eine Typprüfung der Quelldateien. Diese Option ist nur relevant, wenn nicht weiter
Eine Analyse ist erforderlich (da die Typprüfung implizit vor der Analyse erfolgt).
gestartet wird).

-ulevel n
Schleifen syntaktisch abwickeln n Mal vor der Analyse. Das kann ziemlich kostspielig sein
und einige Plugins (z. B. die Wertanalyse) bieten effizientere Möglichkeiten zur Durchführung
das gleiche. Weitere Informationen finden Sie in den jeweiligen Handbüchern. Das kann auch
schleifenweise über aktiviert werden Schleife Pragma abrollen Richtlinie. EIN
negativer Wert für n wird solche Pragmas verhindern.

[-no]-unicode
gibt ACSL-Formeln mit utf8-Zeichen aus. Dies ist die Standardeinstellung. Wenn gegeben
-kein Unicode Option verwendet Frama-C stattdessen die ASCII-Version. Siehe das ACSL-Handbuch
für die Korrespondenz.

-unsichere-Arrays
sehen -sichere-Arrays

[-no]-unspezifizierter-Zugriff
prüft, ob Lese-/Schreibzugriffe in unbestimmter Reihenfolge erfolgen (gemäß C
(Standardvorstellung eines Sequenzpunkts) werden an separaten Orten durchgeführt. Mit
-kein-unspezifizierter-Zugriffgeht davon aus, dass dies immer der Fall ist (dies ist die Standardeinstellung).

-Ausführung
gibt den Versionsstring von Frama-C aus

-warn-decimal-float
warnt, wenn eine Gleitkommakonstante nicht exakt dargestellt werden kann (z. B. 0.1).
kann einer von sein keine, einmal, oder alle

[-no]-warn-undeclared-callee
warnt, wenn eine Funktion aufgerufen wird, bevor sie deklariert wurde (standardmäßig festgelegt).
Frama-C

Plugins spezifisch Optionen

Für jeden Plugin, der Befehl

frama-c -Plugin-Hilfe

gibt die Liste der Optionen an, die für das Plugin spezifisch sind.

EXIT STATUS

0 Erfolgreiche Ausführung

1 Ungültige Benutzereingabe

2 Benutzerunterbrechung (Kill oder Äquivalent)

3 Nicht implementierte Funktion

4 5 6 Interner Fehler

125 Unbekannter Fehler

Ein Exit-Status größer als 2 kann als Fehler (oder als Funktionsanforderung für den Fall) betrachtet werden
des Ausstiegsstatus 3) und kann auf dem BTS von Frama-C gemeldet werden (siehe unten).

VARIABLEN

Es ist möglich, die Orte zu steuern, an denen Frama-C nach seinen Dateien sucht
folgenden Variablen.

FRAMAC_LIB
Das Verzeichnis, in dem die kompilierten Schnittstellen des Kernels installiert sind

FRAMAC_PLUGIN
Das Verzeichnis, in dem Frama-C Standard-Plug-Ins finden kann. Wenn Sie Plugins wünschen
an mehreren Stellen verwenden -Pfad hinzufügen stattdessen.

FRAMAC_SHARE
Das Verzeichnis, in dem Frama-C-Daten installiert sind.

Nutzen Sie frama-c-gui online über die Dienste von onworks.net