sig
val check_call : Cil_types.stmt -> bool -> Cil_types.stmt
val print_select :
Stdlib.Format.formatter ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
val get_select_kf : Cil_types.varinfo * 'a -> Cil_types.kernel_function
val check_db_select :
Cil_datatype.Varinfo.t ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val empty_db_select :
Kernel_function.t -> Cil_types.varinfo * SlicingInternals.fct_user_crit
val top_db_select :
Kernel_function.t ->
SlicingInternals.pdg_mark ->
Cil_types.varinfo * SlicingInternals.fct_user_crit
val check_kf_db_select :
Kernel_function.t ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val check_ff_db_select :
SlicingInternals.fct_slice ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val bottom_msg : Kernel_function.t -> unit
val basic_add_select :
Kernel_function.t ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
PdgTypes.Node.t list ->
?undef:Locations.Zone.t option * SlicingTypes.sl_mark ->
SlicingActions.n_or_d_marks ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_pdg_nodes :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
PdgTypes.Node.t list ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val mk_select :
Db.Pdg.t ->
SlicingActions.select ->
(PdgTypes.Node.t * Locations.Zone.t option) list ->
Locations.Zone.t option ->
SlicingTypes.sl_mark -> SlicingInternals.fct_user_crit
val select_stmt_zone :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.stmt ->
before:bool ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_in_out_zone :
at_end:bool ->
use_undef:bool ->
Kernel_function.t ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_zone_at_end :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_modified_output_zone :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_zone_at_entry :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Locations.Zone.t ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val stmt_nodes_to_select :
Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list
val select_stmt_computation :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.stmt ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_label :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.logic_label ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_minimal_call :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.stmt ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_stmt_ctrl :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.stmt -> Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_entry_point :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_return :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val select_decl_var :
Kernel_function.t ->
?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_types.varinfo ->
SlicingTypes.sl_mark ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
val merge_select :
SlicingInternals.fct_user_crit ->
SlicingInternals.fct_user_crit -> SlicingInternals.fct_user_crit
val merge_db_select :
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
module Selections :
sig
val add_to_selects :
Cil_datatype.Varinfo.Map.key * SlicingInternals.fct_user_crit ->
SlicingInternals.fct_user_crit Cil_datatype.Varinfo.Map.t ->
SlicingInternals.fct_user_crit Cil_datatype.Varinfo.Map.t
val iter_selects_internal :
(Cil_datatype.Varinfo.Map.key * 'a -> unit) ->
'a Cil_datatype.Varinfo.Map.t -> unit
val fold_selects_internal :
('a -> Cil_datatype.Varinfo.Map.key * 'b -> 'a) ->
'a -> 'b Cil_datatype.Varinfo.Map.t -> 'a
end
val add_crit_ff_change_call :
SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.called_fct -> unit
val call_ff_in_caller :
caller:SlicingInternals.fct_slice ->
to_call:SlicingInternals.fct_slice -> unit
val call_fsrc_in_caller :
caller:SlicingInternals.fct_slice -> to_call:Kernel_function.t -> unit
val call_min_f_in_caller :
caller:SlicingInternals.fct_slice ->
to_call:Cil_types.kernel_function -> unit
val is_already_selected :
SlicingInternals.fct_slice ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> bool
val add_ff_selection :
SlicingInternals.fct_slice ->
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
val add_fi_selection :
Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
end