--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on October 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] slicing inquiry



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>