--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on October 2019 ---
Hello Virgile Thank you very much. This is super useful!! I do not know Ocaml, so I would be stuck for a long time if you didn't took the trouble to make this script. There's a couple of corner cases that I will try to solve (i.e conditional statements only show the line where they begin, and function's declaring lines aren't shown as well). I have an spin-off question, how is the recommended way to execute frama-c over a project? (e.g. gzip) that have multiple headers and .c files, and have a makefile for compiling. Cheers Ivan.- On Wed, Oct 2, 2019 at 5:45 AM Virgile Prevosto <virgile.prevosto at m4x.org> wrote: > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191002/b6503ef5/attachment.html>