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

[Frama-c-discuss] slicing inquiry



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>