Kann frama-c für die Header-Dateianalyse verwendet werden?

Question

Ich betrachtete frama-c als eine Möglichkeit, C-Header-Dateien in OCaml zu verarbeiten (z. B. zum Generieren von Sprachbindungen). Es ist attraktiv, weil es wie ein sehr gut dokumentiertes und gepflegtes Projekt aussieht. Nach vielem Googeln und Durchsuchen der Dokumentation kann ich jedoch nichts passendes finden. Fehle ich gerade den richtigen Weg, oder ist es außerhalb des Rahmens von frama-c? Es scheint eine ziemlich triviale Sache zu sein, verglichen mit einigen anderen Plugins.

Answer 1

Wie Pascal gesagt, ich glaube nicht, dass es möglich ist, von der Befehlszeile aus, aber da Sie sowieso etwas Code schreiben müssen, können Sie das Flag Rmtmps.keepUnused setzen. Dies ist ein Skript, das Sie die Deklarationen verwenden können, um zu sehen:

let main() = 
    Rmtmps.keepUnused := true; 
    let file = File.from_filename "t.h" in 
    let() = File.init_from_c_files [ file ] in 
    let _ast = Ast.get() in 
    let show_function f = 
    let name = Kernel_function.get_name f in 
    if not (Cil.Builtin_functions.mem name) then 
     Format.printf "Function @[<2>%a:@ @[@[type: %a@]@ @[%s at %a@]@]@]@." 
     Kernel_function.pretty f 
     Cil_datatype.Typ.pretty (Kernel_function.get_type f) 
     (if Kernel_function.is_definition f then "defined" else "declared") 
     Cil.d_loc (Kernel_function.get_location f) 
in Globals.Functions.iter show_function 

let() = Db.Main.extend main 

es ausführen zu können, müssen Sie die -load-script Option wie folgt verwenden:

$ frama-c -load-script script.ml 

Entwicklung eines Plug-in wird besser geeignet sein für komplexere Verarbeitung (siehe Entwicklerhandbuch dafür), aber ein Skript macht es einfach zu testen.

Answer 2

Im aktuellen Zustand würde ich sagen, dass es leider unmöglich ist, Frama-C zu verwenden, um Deklarationen von Funktionen zu analysieren, die weder definiert noch verwendet werden.

t.h:

int mybinding (int x, int y); 

Dies gibt Ihnen einen Blick auf das normalisierte AST. Normalized bedeutet, dass alles, was war vereinfacht werden könnte:

$ frama-c -print t.h 
[kernel] preprocessing with "gcc -C -E -I. t.h" 
/* Generated by Frama-C */ 

Und leider, da mybinding weder verwendet noch definiert, es wurde gelöscht.

Es gibt eine Option, Deklarationen mit Spezifikationen zu halten, aber was Sie wollen, ist eine Option, alle Deklarationen zu behalten. Ich habe nie bemerkt, eine solche Option:

$ frama-c -kernel-help 
... 
-keep-unused-specified-functions keep specified-but-unused functions (set by 
        default, opposite option is 
        -remove-unused-specified-functions) 

Und die Möglichkeit, Funktionen mit Spezifikationen zu halten nicht, was Sie wollen:

$ frama-c -keep-unused-specified-functions -print t.h 
[kernel] preprocessing with "gcc -C -E -I. t.h" 
/* Generated by Frama-C */