Frama-C API - SlicingSelect
val check_call : Frama_c_kernel.Cil_types.stmt -> bool -> Frama_c_kernel.Cil_types.stmtval print_select : Stdlib.Format.formatter -> SlicingTypes.sl_select -> unitval 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 top_db_select : Frama_c_kernel.Kernel_function.t -> SlicingInternals.pdg_mark -> 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 bottom_msg : Frama_c_kernel.Kernel_function.t -> unitval 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_selectmodule Selections : sig ... endval 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 -> unitval is_already_selected : SlicingInternals.fct_slice -> SlicingTypes.sl_select -> boolval add_ff_selection : SlicingInternals.fct_slice -> SlicingTypes.sl_select -> unitval add_fi_selection : SlicingTypes.sl_select -> unitadd a persistent selection to the function. This might change its slicing level in order to call slices later on.