Slicing.SlicingSelect
val check_call :
Frama_c_kernel.Cil_types.stmt ->
bool ->
Frama_c_kernel.Cil_types.stmt
val print_select : Stdlib.Format.formatter -> SlicingTypes.sl_select -> unit
val get_select_kf :
(Frama_c_kernel.Cil_types.varinfo * 'a) ->
Frama_c_kernel.Cil_types.kernel_function
val check_db_select :
Frama_c_kernel.Cil_datatype.Varinfo.t ->
SlicingTypes.sl_select ->
SlicingTypes.sl_select
val empty_db_select :
Frama_c_kernel.Kernel_function.t ->
Frama_c_kernel.Cil_types.varinfo * SlicingInternals.fct_user_crit
val top_db_select :
Frama_c_kernel.Kernel_function.t ->
SlicingInternals.pdg_mark ->
Frama_c_kernel.Cil_types.varinfo * SlicingInternals.fct_user_crit
val check_kf_db_select :
Frama_c_kernel.Kernel_function.t ->
SlicingTypes.sl_select ->
SlicingTypes.sl_select
val check_ff_db_select :
SlicingInternals.fct_slice ->
SlicingTypes.sl_select ->
SlicingTypes.sl_select
val bottom_msg : Frama_c_kernel.Kernel_function.t -> unit
val basic_add_select :
Frama_c_kernel.Kernel_function.t ->
SlicingTypes.sl_select ->
Pdg_types.PdgTypes.Node.t list ->
?undef:(Frama_c_kernel.Locations.Zone.t option * SlicingTypes.sl_mark) ->
SlicingActions.n_or_d_marks ->
SlicingTypes.sl_select
val select_pdg_nodes :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Pdg_types.PdgTypes.Node.t list ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
val mk_select :
Pdg.Api.t ->
SlicingActions.select ->
(Pdg_types.PdgTypes.Node.t * Frama_c_kernel.Locations.Zone.t option) list ->
Frama_c_kernel.Locations.Zone.t option ->
SlicingTypes.sl_mark ->
SlicingInternals.fct_user_crit
val select_stmt_zone :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.stmt ->
before:bool ->
Frama_c_kernel.Locations.Zone.t ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
val select_in_out_zone :
at_end:bool ->
use_undef:bool ->
Frama_c_kernel.Kernel_function.t ->
SlicingTypes.sl_select ->
Frama_c_kernel.Locations.Zone.t ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
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 :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Locations.Zone.t ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
val select_modified_output_zone :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Locations.Zone.t ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
val select_zone_at_entry :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Locations.Zone.t ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
val stmt_nodes_to_select :
Pdg.Api.t ->
Frama_c_kernel.Cil_types.stmt ->
Pdg_types.PdgTypes.Node.t list
val select_stmt_computation :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.stmt ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
val select_label :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.logic_label ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
val select_minimal_call :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.stmt ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
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 :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.stmt ->
SlicingTypes.sl_select
val select_entry_point :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
val select_return :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
val select_decl_var :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.varinfo ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_select
val merge_select :
SlicingInternals.fct_user_crit ->
SlicingInternals.fct_user_crit ->
SlicingInternals.fct_user_crit
val merge_db_select :
SlicingTypes.sl_select ->
SlicingTypes.sl_select ->
SlicingTypes.sl_select
module Selections : sig ... end
val add_crit_ff_change_call :
SlicingInternals.fct_slice ->
Frama_c_kernel.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:Frama_c_kernel.Kernel_function.t ->
unit
val call_min_f_in_caller :
caller:SlicingInternals.fct_slice ->
to_call:Frama_c_kernel.Cil_types.kernel_function ->
unit
val is_already_selected :
SlicingInternals.fct_slice ->
SlicingTypes.sl_select ->
bool
val add_ff_selection :
SlicingInternals.fct_slice ->
SlicingTypes.sl_select ->
unit
val add_fi_selection : SlicingTypes.sl_select -> unit
add a persistent selection to the function. This might change its slicing level in order to call slices later on.