module SlicingActions:sig
..end
selection mode (ie which mark to associate to the node
and how to propagate in the different kinds of dependencies)
val build_simple_node_selection : ?nd_marks:(SlicingInternals.node_or_dpds * 'a) list ->
'a -> (SlicingInternals.node_or_dpds * 'a) list
SlicingActions.build_node_and_dpds_selection
)val build_addr_dpds_selection : ?nd_marks:(SlicingInternals.node_or_dpds * 'a) list ->
'a -> (SlicingInternals.node_or_dpds * 'a) list
val build_data_dpds_selection : ?nd_marks:(SlicingInternals.node_or_dpds * 'a) list ->
'a -> (SlicingInternals.node_or_dpds * 'a) list
val build_ctrl_dpds_selection : ?nd_marks:(SlicingInternals.node_or_dpds * 'a) list ->
'a -> (SlicingInternals.node_or_dpds * 'a) list
val build_node_and_dpds_selection : ?nd_marks:(SlicingInternals.node_or_dpds * SlicingTypes.sl_mark) list ->
SlicingTypes.sl_mark ->
(SlicingInternals.node_or_dpds * SlicingTypes.sl_mark) list
SlicingTypes.Internals.node_or_dpds
).
This description depend on the mark that has been asked for.
First of all, whatever the mark is, the node is selected as spare
,
so that it will be visible, and so will its dependencies. Then,
if is_ctrl mark
propagate a m1 control mark through the control dependencies
and do a similar thing for addr
and data
val translate_crit_to_select : PdgTypes.Pdg.t ->
?to_select:'a PdgMarks.select ->
((PdgTypes.Node.t * Locations.Zone.t option) list *
(SlicingInternals.node_or_dpds * 'a) list)
list -> 'a PdgMarks.select
val mk_fct_crit : SlicingInternals.fct_info ->
SlicingInternals.fct_crit -> SlicingInternals.criterion
val mk_fct_user_crit : SlicingInternals.fct_info ->
SlicingInternals.fct_user_crit -> SlicingInternals.criterion
val mk_crit_fct_top : SlicingInternals.fct_info ->
SlicingInternals.pdg_mark -> SlicingInternals.criterion
val mk_crit_fct_user_select : SlicingInternals.fct_info ->
SlicingInternals.pdg_mark PdgMarks.select -> SlicingInternals.criterion
val mk_crit_prop_persit_marks : SlicingInternals.fct_info ->
SlicingInternals.pdg_mark PdgMarks.select -> SlicingInternals.criterion
val mk_ff_crit : SlicingInternals.fct_slice ->
SlicingInternals.fct_crit -> SlicingInternals.criterion
val mk_ff_user_select : SlicingInternals.fct_slice ->
SlicingInternals.pdg_mark PdgMarks.select -> SlicingInternals.criterion
val mk_crit_choose_call : SlicingInternals.fct_slice -> Cil_types.stmt -> SlicingInternals.criterion
val mk_crit_change_call : SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.called_fct -> SlicingInternals.criterion
val mk_crit_missing_inputs : SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.pdg_mark PdgMarks.select * bool ->
SlicingInternals.criterion
val mk_crit_missing_outputs : SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.pdg_mark PdgMarks.select * bool ->
SlicingInternals.criterion
val mk_crit_examines_calls : SlicingInternals.fct_slice ->
SlicingInternals.pdg_mark PdgMarks.info_called_outputs ->
SlicingInternals.criterion
val mk_appli_select_calls : SlicingInternals.fct_info -> SlicingInternals.criterion
val mk_crit_mark_calls : SlicingInternals.fct_info ->
Cil_types.kernel_function ->
SlicingInternals.pdg_mark -> SlicingInternals.criterion
val mk_crit_add_output_marks : SlicingInternals.fct_slice ->
SlicingInternals.pdg_mark PdgMarks.select -> SlicingInternals.criterion
val print_nd_and_mark : Format.formatter ->
SlicingInternals.node_or_dpds * SlicingTypes.sl_mark -> unit
val print_nd_and_mark_list : Format.formatter ->
(SlicingInternals.node_or_dpds * SlicingTypes.sl_mark) list -> unit
val print_nodes : Format.formatter -> PdgTypes.Node.t list -> unit
val print_node_mark : Format.formatter ->
PdgTypes.Node.t -> Locations.Zone.t option -> SlicingTypes.sl_mark -> unit
val print_sel_marks_list : Format.formatter ->
(PdgMarks.select_elem * SlicingTypes.sl_mark) list -> unit
val _print_ndm : Format.formatter ->
PdgTypes.Node.t list *
(SlicingInternals.node_or_dpds * SlicingTypes.sl_mark) list -> unit
val print_f_crit : Format.formatter -> SlicingInternals.fct_user_crit -> unit
val print_crit : Format.formatter -> SlicingInternals.criterion -> unit
val print_list_crit : Format.formatter -> SlicingInternals.criterion list -> unit