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

  • Subject: [Frama-c-discuss] slicing inquiry
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Wed, 2 Oct 2019 10:44:16 +0200
  • In-reply-to: <CALVmTfvp2FTfwFJ_u3AsqWyN0=KnQDOZmcNvyCYiXLvthmr1AA@mail.gmail.com>
  • References: <CALVmTfueJw4zsSyaNmS8bE0P4TZvHcwWct7EfSmYbxKMOfzQuQ@mail.gmail.com> <CA+yPOVjAqm=S5M1P0sD3tq3SGMKTf+_zOGpWiN1J919tZ1-fnQ@mail.gmail.com> <CALVmTfvp2FTfwFJ_u3AsqWyN0=KnQDOZmcNvyCYiXLvthmr1AA@mail.gmail.com>
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
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191002/5689334f/attachment.html>