How to use this function Db.Slicing.Select.select_stmt with frama-C

The function which is in the title has the following signature:

val select_stmt :
 (set -> spare:bool -> Cil_types.stmt -> Cil_types.kernel_function -> set)
   Pervasives.ref

I would like to use this function but my problem is about the argument set which has type type set = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t. I don't know exactly how to initialize this parameter and after that I would like to print the result.

Solution

Just above select_stmt, you have the value empty_selects, whose documentation indicate that it represents an empty selection. After that, Slicing's API is a bit arcane but if I'm not mistaken, you should be able to obtain a slice with something along the following lines (not tested):

let prj =
 Db.Slicing.(
  let sp = !Project.mk_project "my slicing project" in
  let selection = Select.(!select_stmt empty_selects s kf) in
  let () = Request.add_selection sp selection in
  Project.extract "my frama-c project" sp)
in
File.pretty_ast ~prj ()

Basically, you have to create a slicing project, on which you can set a certain number of options, including in particular the slicing criterion you want. When you're satisfied with the state of your slicing project, you can extract a new Frama-C project from it, and pretty-prints this new project normally (you can of course also perform other analyses on it).