Slicing.Fct_slice
val is_src_fun_called : Frama_c_kernel.Cil_types.kernel_function -> bool
Return true
if the source function is called (even indirectly via transitivity) from a Slice.t
.
val is_src_fun_visible : Frama_c_kernel.Cil_types.kernel_function -> bool
Return true
if the source function is visible (even indirectly via transitivity) from a Slice.t
.
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 ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.fct_slice ->
SlicingInternals.criterion list
val apply_change_call :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.called_fct ->
SlicingInternals.criterion list
val apply_choose_call :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.criterion list
val apply_missing_inputs :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
(SlicingInternals.fct_base_criterion * bool) ->
SlicingInternals.criterion list
val apply_missing_outputs :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.fct_base_criterion ->
bool ->
SlicingInternals.criterion list
val apply_examine_calls :
SlicingInternals.fct_slice ->
SlicingInternals.pdg_mark Pdg_types.PdgMarks.info_called_outputs ->
SlicingInternals.criterion list
val get_called_slice :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.fct_slice option * bool
val get_node_mark :
SlicingInternals.fct_slice ->
Pdg_types.PdgTypes.Node.t ->
SlicingInternals.pdg_mark
val get_node_key_mark :
SlicingInternals.fct_slice ->
Pdg_types.PdgIndex.Key.t ->
SlicingInternals.pdg_mark
val get_top_input_mark : SlicingInternals.fct_info -> SlicingInternals.pdg_mark
val get_stmt_mark :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.pdg_mark
val get_label_mark :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.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 ->
Frama_c_kernel.Cil_types.varinfo ->
SlicingInternals.pdg_mark
val get_input_loc_under_mark :
SlicingInternals.fct_slice ->
Frama_c_kernel.Locations.Zone.t ->
SlicingInternals.pdg_mark
val get_mark_from_src_fun :
Frama_c_kernel.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 :
Stdlib.Format.formatter ->
SlicingInternals.fct_slice ->
unit