Slicing.SlicingSelectSourceval get_select_kf :
(Frama_c_kernel.Cil_types.varinfo * 'a) ->
Frama_c_kernel.Cil_types.kernel_functionval check_db_select :
Frama_c_kernel.Cil_datatype.Varinfo.t ->
SlicingTypes.sl_select ->
SlicingTypes.sl_selectval empty_db_select :
Frama_c_kernel.Kernel_function.t ->
Frama_c_kernel.Cil_types.varinfo * SlicingInternals.fct_user_critval check_kf_db_select :
Frama_c_kernel.Kernel_function.t ->
SlicingTypes.sl_select ->
SlicingTypes.sl_selectval check_ff_db_select :
SlicingInternals.fct_slice ->
SlicingTypes.sl_select ->
SlicingTypes.sl_selectval 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_selectval select_pdg_nodes :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Pdg_types.PdgTypes.Node.t list ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_selectval 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_critval 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_selectval 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_selectthis 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_selectval 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_selectval 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_selectval stmt_nodes_to_select :
Pdg.Api.t ->
Frama_c_kernel.Cil_types.stmt ->
Pdg_types.PdgTypes.Node.t listval select_stmt_computation :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.stmt ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_selectval select_label :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.logic_label ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_selectval select_minimal_call :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.stmt ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_selectmarking 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_selectval select_entry_point :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_selectval select_return :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_selectval select_decl_var :
Frama_c_kernel.Kernel_function.t ->
?select:SlicingTypes.sl_select ->
Frama_c_kernel.Cil_types.varinfo ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_selectval merge_select :
SlicingInternals.fct_user_crit ->
SlicingInternals.fct_user_crit ->
SlicingInternals.fct_user_critval merge_db_select :
SlicingTypes.sl_select ->
SlicingTypes.sl_select ->
SlicingTypes.sl_selectval add_crit_ff_change_call :
SlicingInternals.fct_slice ->
Frama_c_kernel.Cil_types.stmt ->
SlicingInternals.called_fct ->
unitval call_ff_in_caller :
caller:SlicingInternals.fct_slice ->
to_call:SlicingInternals.fct_slice ->
unitchange 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 ->
unitval call_min_f_in_caller :
caller:SlicingInternals.fct_slice ->
to_call:Frama_c_kernel.Cil_types.kernel_function ->
unitadd a persistent selection to the function. * This might change its slicing level in order to call slices later on.