Module SlicingActions

module SlicingActions: sig .. end

This module deals with the action management. It consiste of the definitions of the different kind of actions, and the management of the action list.

selection mode (ie which mark to associate to the node and how to propagate in the different kinds of dependencies)

Build

How the elements will be selected

val build_simple_node_selection : ?nd_marks:(SlicingInternals.node_or_dpds * 'a) list ->
       'a -> (SlicingInternals.node_or_dpds * 'a) list

Build a description to tell that the associated nodes have to be marked with the given mark, and than the same one will be propagated through their dependencies. (see also 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

Only the control dependencies of the nodes will be marked

val build_data_dpds_selection : ?nd_marks:(SlicingInternals.node_or_dpds * 'a) list ->
       'a -> (SlicingInternals.node_or_dpds * 'a) list

Only the control dependencies of the nodes will be marked

val build_ctrl_dpds_selection : ?nd_marks:(SlicingInternals.node_or_dpds * 'a) list ->
       'a -> (SlicingInternals.node_or_dpds * 'a) list

Only the control dependencies of the nodes will be marked

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

Build a description to tell how the selected PDG nodes and their dependencies will have to be marked (see 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

Translations to a mapping between marks and program elements

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

Function criteria

val mk_fct_crit : SlicingInternals.fct_info ->
       SlicingInternals.fct_crit -> SlicingInternals.criterion

build an action to apply the criteria to the persistent selection of the function. It means that it will be applied to all slices.

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

build an action to apply the criteria to the given slice.

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

Shortcut functions for previous things

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

Print

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

Printing

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