Can frama-c be used to parse header files?

Question

I saw frama-c as a way to handle C header files in OCaml (for example, to create language bindings). This is attractive because it looks like a very well documented and supported project. However, after a lot of searches and documentation, I can’t find anything suitable for this purpose. Am I just missing the right way to do this, or is it out of scope? This seems to be pretty trivial compared to some other plugins.

Answer 1

As Pascal said, I don’t think it’s possible from the command line, but since you still have to write some code, you can set the Rmtmps.keepUnused flag. This is a script that you can use to view ads:

 let main () = Rmtmps.keepUnused := true; let file = File.from_filename "th" 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 

To run it, you must use the -load-script parameter as follows:

 $ frama-c -load-script script.ml 

Plugin development will be more suitable for more complex processing (see the Developer's Guide for this), but the script makes it easy to test.

Answer 2

In the current state, I would say that, unfortunately, it is impossible to use Frama-C to analyze declarations of functions that are not defined or not used.

th:

 int mybinding (int x, int y); 

This gives you an idea of ​​normalized AST. Normalized means that everything that could be simplified was:

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

And unfortunately, since mybinding not used and was not defined, it was deleted.

It is possible to save ads with specifications, but you want to save all ads. I have never noticed such an option:

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

And the option to save functions with specifications does not do what you want:

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