--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on October 2019 ---
Hello, Le lun. 30 sept. 2019 à 18:11, Ivan Postolski <ivan.postolski at gmail.com> a écrit : > > Thanks for the fast reply. I'm running frama-c from the command line. Do > you know where should I look for this meta-data? > > This information is stored in Frama-C's internal datastructures (namely the Abstract Syntax Tree, AST). To obtain it, you'll have to attack Frama-C's API and write an OCaml script. In order to obtain something that does exactly what you want, you will probably need to have a look at the developer manual ( http://frama-c.com/download/plugin-development-guide-19.1-Potassium.pdf), but here is a small script that will just print on the standard output the location of the statements: --------- script.ml open Cil_types open Cil include Plugin.Register( struct let name = "display-loc" let shortname = "dl" let help = "quick demo plug-in for displaying location info" end) module Output = False( struct let option_name = "-display-loc" let help = "display location of all statements" end) class display_location = object inherit Visitor.frama_c_inplace method! vglob_aux g = match g with | GFun(f,_) -> Format.printf "Now considering function %s at ." f.svar.vorig_name; DoChildren | _ -> SkipChildren method! vstmt_aux s = let loc = Cil_datatype.Stmt.loc s in Format.printf "Kept statement at %a:@\n%a at ." Printer.pp_location loc Printer.pp_stmt s; DoChildren end let print_sliced () = if Output.get () then Visitor.visitFramacFileSameGlobals (new display_location) (Ast.get()) let () = Db.Main.extend print_sliced --------------- We register it as a plugin in order to be able to register a new option `-display-loc` to control whether the print should occur in `print_sliced`, the main entry point of the plugin, which in turn gets registered in Frama-C's own main entry point. This option is useful to ensure that `print_sliced` is called only on the projects we are interested in by using the `-then*` options of the command-line to properly sequence the things Frama-C should do. A call to Frama-C would then be along those lines: frama-c -load-script script.ml file1.c file2.c -slice-return main -then-last -display-loc Best regards, -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191002/5689334f/attachment.html>