--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on October 2019 ---
On 02/10/2019 18:26, Ivan Postolski wrote: > 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. I did some blog posts on the subject, for instance: http://blog.frama-c.com/index.php?post/2018/01/25/Analysis-scripts%3A-helping-automate-case-studies There are some newer features in the latest Frama-C releases that could help. Namely, frama-c-script. But the overall process is not perfectly robust: we rely on the JSON Compilation Database <https://clang.llvm.org/docs/JSONCompilationDatabase.html> format used by LLVM, which is not ideal, so a few caveats apply. Overall, the process is: - Install Build EAR <https://github.com/rizsotto/Bear> to generate a compile_commands.json file from running gzip's makefile (e.g. `bear make`); - Run `frama-c-script list-files` to list the available source files (including the ones containing a main function); - Run `frama-c-script make-template` to create a GNUmakefile template for running Frama-C; - If everything works as expected, running `make parse` should parse the files with Frama-C, then `make eva` should run the Eva plug-in. If you want to use other plug-ins, you can load the parsing result and apply other command-line options, e.g.: frama-c -load gzip.parse/framac.sav <other options> (if you want to reuse the results /after/ running Eva, just load gzip.*eva*/framac.sav instead) By the way, there is a Github repository with open source case studies for Eva <https://github.com/Frama-C/open-source-case-studies> which includes an old version of gzip. The case study is not finalized, but it could serve as example on how to configure things. You can take a look at `gzip124/GNUmakefile`. Best regards, André > Cheers > > Ivan.- > > > On Wed, Oct 2, 2019 at 5:45 AM Virgile Prevosto > <virgile.prevosto at m4x.org <mailto:virgile.prevosto at m4x.org>> wrote: > > Hello, > > Le lun. 30 sept. 2019 à  18:11, Ivan Postolski > <ivan.postolski at gmail.com <mailto: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 <http://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 <http://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 > <mailto:Frama-c-discuss at lists.gforge.inria.fr> > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -- André Maroneze Researcher/Engineer CEA/List Software Reliability and Security Laboratory -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191002/d6cd3b68/attachment-0001.html>