Search code examples
cstatic-analysisframa-c

How to save types of variables to a file using Frama-C

I am trying to print types of variables in C program using Frama-C. I found that this information is represented in the GUI as in the figure below. However, I cannot found a way to output this information to a file. Could you please suggest me the way to perform this task with Frama-c? enter image description here

Solution

  • There are no direct solutions from the command line. However, this can be very easily done with a simple script such as (not tested)

    let print_type () =
  Ast.compute();
  Globals.Vars.iter
   (fun v _ ->
     Format.printf "Variable %a: %a@."
     Cil_datatype.Varinfo.pretty v
     Cil_datatype.Typ.pretty v.vtype)

let () = Db.Main.extend print_type

    which can be launched with frama-c -load-script <my_script.ml> <other args including source files>

    More information on scripting Frama-C (including an extensive tutorial) is available in the developer manual.