Frama-C-Code-Slicer lädt keine C-Dateien

Question

Ich habe eine 1000 Zeilen C-Datei mit 10 mathematischen Algorithmen von einem Professor geschrieben, muss ich 9 mathematische Funktionen und alle ihre Abhängigkeiten von den 1000 Zeilen löschen, so habe ich eine Verwenden Sie Frama-C Bor Windows-Binär-Installer.

Jetzt wird es nicht laden die einfachste Beispiel.c-Datei ... ich wähle Quelldatei und nichts lädt.

Bor Ausgabe ist von 2010, also habe ich überprüft, wie man eine spätere Frama-C kompilieren: sie sagen, ein Leerzeichen in meinem Windows 7 Benutzernamen kann Probleme verursachen, die nicht ermutigend ist.

Ist Frama-C meine beste Option für meine Slicing-Aufgabe?

Hier eine Beispieldatei, die nicht geladen werden kann:

// File swap.c: 

    /*@ requires \valid(a) && \valid(b); 
     @ ensures A: *a == \old(*b) ; 
     @ ensures B: *b == \old(*a) ; 
     @ assigns *a,*b ; 
     @*/ 
    void swap(int *a,int *b) 
    { 
     int tmp = *a ; 
     *a = *b ; 
     *b = tmp ; 
     return ; 
    } 

Hier ist der Code ich wünsche nur von einer Funktion zu übernehmen, markiert die Option glatt und swvd. https://sites.google.com/site/kootsoop/Home/cohens_class_code

Answer 1

Ich habe mir den Code angesehen, den Sie verlinkt haben, und es scheint nicht der beste Kandidat für eine Frama-C-Analyse zu sein. Zum Beispiel ist dieser Code nicht streng C99-konform, wobei z.B. einige alte Prototypen (einschließlich impliziter int Rückgabetypen), Funktionen, die verwendet werden, bevor sie ohne Forward-Deklarationen (fft) definiert werden, und eine fehlende Header-Einschluss (stdlib.h). Das sind keine großen Probleme, da die Änderungen relativ einfach sind und einige von ihnen ähnlich behandelt werden, wie gcc -std=c99 funktioniert: Sie geben Warnungen, aber keine Fehler aus. Es ist jedoch wichtig zu beachten, dass sie eine Zeitspanne ungleich Null benötigen, daher ist dies keine "Plug-and-Play" -Lösung.

Auf eine allgemeinere Anmerkung, Frama-C stützt sich auf CIL (C Intermediate Language) für C-Code-Normalisierung, so dass das geschnittene Programm wird wahrscheinlich nicht identisch mit "das ursprüngliche Programm minus die geschnittenen Aussagen". Wenn das Ziel nur darin besteht, einige Anweisungen zu entfernen, aber den Code ansonsten syntaktisch identisch zu halten, dann ist Frama-C nicht ideal .

Schließlich ist es erwähnenswert, dass einige Frama-C-Analysen helfen können, toten Code zu finden, und das Ergebnis ist noch klarer, wenn der Code bereits in Funktionen aufgeteilt ist. Wenn Sie beispielsweise die Wertanalyse für ein ordnungsgemäß konfiguriertes Programm verwenden, können Sie sehen, welche Anweisungen/Funktionen nie ausgeführt werden. Aber dies beruht auf der Abwesenheit von zumindest einigen Arten von undefiniertem Verhalten.

z. Wenn in Ihrem Programm nicht initialisierte Variablen verwendet werden (was durch den C-Standard verboten ist, aber gelegentlich geschieht und unbemerkt bleibt), wird die Propagierung der Wertanalyse gestoppt und der Code kann danach als tot markiert werden, da er semantisch tot w.r.t. Der Standard. Es ist wichtig, sich dessen bewusst zu sein, da ein naives Vorgehen irreführend wäre.

Insgesamt, für die Code-Größe, die Sie erwähnen, bin ich nicht sicher Frama-C wäre eine kostengünstige Lösung, vor allem wenn (1) Sie Frama-C nie verwendet haben und Probleme haben, es zu kompilieren (Bor ist eine wirklich alte Version, nicht empfohlen) und (2) wenn Sie Ihre Codebasis bereits kennen und daher die Teile manuell schneiden könnten.

Das gesagt, ich kenne keinen C-Slicer, der solche Anweisungen bewahrt; Mein Punkt ist, dass, obwohl man intuitiv denken könnte, dass ein C-Slicer den Großteil der Syntax einfach bewahren würde, C eine so hinterhältige Sprache ist, dass dies sehr schwierig ist, weshalb die meisten Tools vorher einige Normalisierungsschritte durchführen.