Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>