--- layout: fc_discuss_archives title: Message 1 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,

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>