module Fct_slice:sig
..end
true
if the source function is called
(even indirectly via transitivity) from a Slice.t
.
This module deals with slice computation.
It computes a mapping between the PDG nodes and some marks
(see Fct_slice.FctMarks
),
and also manage interprocedural propagation (Fct_slice.CallInfo
).
Most high level function, named apply_xxx
,
like apply_change_call
, apply_missing_outputs
, ...,
correspond the actions defined in the
specification report.
Many functions are modifying the marks of a slice, so they can return a list of actions to be applied in order to deal with the propagation in the calls and callers.
Moreover, some function (named get_xxx_mark
) are provided to retrieve
the mark of the slice elements.
val is_src_fun_called : Cil_types.kernel_function -> bool
true
if the source function is called
(even indirectly via transitivity) from a Slice.t
.val is_src_fun_visible : Cil_types.kernel_function -> bool
true
if the source function is visible
(even indirectly via transitivity) from a Slice.t
.SlicingTypes.ExternalFunction
if the function has no source code,
because there cannot be any slice for it.SlicingTypes.NoPdg
when there is no PDG for the function.val make_new_ff : SlicingInternals.fct_info ->
bool -> SlicingInternals.fct_slice * SlicingInternals.criterion list
val merge_slices : SlicingInternals.fct_slice ->
SlicingInternals.fct_slice ->
SlicingInternals.fct_slice * SlicingInternals.criterion list
val copy_slice : SlicingInternals.fct_slice -> SlicingInternals.fct_slice
val filter_already_in : SlicingInternals.fct_slice ->
SlicingInternals.fct_base_criterion -> SlicingInternals.fct_base_criterion
val apply_add_marks : SlicingInternals.fct_slice ->
SlicingInternals.fct_base_criterion -> SlicingInternals.criterion list
val add_marks_to_fi : SlicingInternals.fct_info ->
SlicingInternals.fct_base_criterion ->
bool ->
SlicingInternals.criterion list -> bool * SlicingInternals.criterion list
val add_top_mark_to_fi : SlicingInternals.fct_info ->
SlicingInternals.pdg_mark ->
bool -> SlicingInternals.criterion list -> SlicingInternals.criterion list
val check_outputs_before_change_call : SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.fct_slice -> SlicingInternals.criterion list
val apply_change_call : SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.called_fct -> SlicingInternals.criterion list
val apply_choose_call : SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.criterion list
val apply_missing_inputs : SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.fct_base_criterion * bool -> SlicingInternals.criterion list
val apply_missing_outputs : SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.fct_base_criterion ->
bool -> SlicingInternals.criterion list
val apply_examine_calls : SlicingInternals.fct_slice ->
SlicingInternals.pdg_mark PdgMarks.info_called_outputs ->
SlicingInternals.criterion list
val get_called_slice : SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.fct_slice option * bool
val get_node_mark : SlicingInternals.fct_slice -> PdgTypes.Node.t -> SlicingInternals.pdg_mark
val get_node_key_mark : SlicingInternals.fct_slice -> PdgIndex.Key.t -> SlicingInternals.pdg_mark
val get_top_input_mark : SlicingInternals.fct_info -> SlicingInternals.pdg_mark
val get_stmt_mark : SlicingInternals.fct_slice -> Cil_types.stmt -> SlicingInternals.pdg_mark
val get_label_mark : SlicingInternals.fct_slice ->
Cil_types.stmt -> Cil_types.label -> SlicingInternals.pdg_mark
val get_param_mark : SlicingInternals.fct_slice -> int -> SlicingInternals.pdg_mark
val get_local_var_mark : SlicingInternals.fct_slice -> Cil_types.varinfo -> SlicingInternals.pdg_mark
val get_input_loc_under_mark : SlicingInternals.fct_slice -> Locations.Zone.t -> SlicingInternals.pdg_mark
val get_mark_from_src_fun : Kernel_function.t -> SlicingInternals.pdg_mark
val merge_inputs_m1_mark : SlicingInternals.fct_slice -> SlicingInternals.pdg_mark
val clear_ff : SlicingInternals.fct_slice -> unit
val print_ff_sig : Format.formatter -> SlicingInternals.fct_slice -> unit