Module SlicingSelect

module SlicingSelect: sig .. end

For internal use




For internal use


val check_call : Cil_types.stmt -> bool -> Cil_types.stmt
val print_select : 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_fi_db_select : SlicingInternals.fct_info ->
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
this one is similar to select_stmt_zone with the return statement when the function is defined, but it can also be used for undefined functions.
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
marking a call node means that a choose_call will have to decide that to call according to the slicing-level, but anyway, the call will be visible.
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 .. 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
change the call to call the given slice. This is a user request, so it might be the case that the new function doesn't compute enough outputs : in that case, add outputs first.
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
add a persistent selection to the function. This might change its slicing level in order to call slices later on.