Module `Slicing.SlicingSelect`Source

Source

val check_call : 
  Frama_c_kernel.Cil_types.stmt ->
  bool ->
  Frama_c_kernel.Cil_types.stmt

Sourceval print_select : Format.formatter -> SlicingTypes.sl_select -> unit

Source

val get_select_kf : 
  (Frama_c_kernel.Cil_types.varinfo * 'a) ->
  Frama_c_kernel.Cil_types.kernel_function

Source

val check_db_select : 
  Frama_c_kernel.Cil_datatype.Varinfo.t ->
  SlicingTypes.sl_select ->
  SlicingTypes.sl_select

Source

val empty_db_select : 
  Frama_c_kernel.Kernel_function.t ->
  Frama_c_kernel.Cil_types.varinfo * SlicingInternals.fct_user_crit

Source

val top_db_select : 
  Frama_c_kernel.Kernel_function.t ->
  SlicingInternals.pdg_mark ->
  Frama_c_kernel.Cil_types.varinfo * SlicingInternals.fct_user_crit

Source

val check_kf_db_select : 
  Frama_c_kernel.Kernel_function.t ->
  SlicingTypes.sl_select ->
  SlicingTypes.sl_select

Source

val check_ff_db_select : 
  SlicingInternals.fct_slice ->
  SlicingTypes.sl_select ->
  SlicingTypes.sl_select

Sourceval bottom_msg : Frama_c_kernel.Kernel_function.t -> unit

Source

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

Source

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

Source

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

Source

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

Source

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.

Source

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

Source

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

Source

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

Source

val stmt_nodes_to_select : 
  Pdg.Api.t ->
  Frama_c_kernel.Cil_types.stmt ->
  Pdg_types.PdgTypes.Node.t list

Source

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

Source

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

Source

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.

Source

val select_stmt_ctrl : 
  Frama_c_kernel.Kernel_function.t ->
  ?select:SlicingTypes.sl_select ->
  Frama_c_kernel.Cil_types.stmt ->
  SlicingTypes.sl_select

Source

val select_entry_point : 
  Frama_c_kernel.Kernel_function.t ->
  ?select:SlicingTypes.sl_select ->
  SlicingTypes.sl_mark ->
  SlicingTypes.sl_select

Source

val select_return : 
  Frama_c_kernel.Kernel_function.t ->
  ?select:SlicingTypes.sl_select ->
  SlicingTypes.sl_mark ->
  SlicingTypes.sl_select

Source

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

Source

val merge_select : 
  SlicingInternals.fct_user_crit ->
  SlicingInternals.fct_user_crit ->
  SlicingInternals.fct_user_crit

Source

val merge_db_select : 
  SlicingTypes.sl_select ->
  SlicingTypes.sl_select ->
  SlicingTypes.sl_select

Sourcemodule Selections : sig ... end

Source

val add_crit_ff_change_call : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  SlicingInternals.called_fct ->
  unit

Source

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.

Source

val call_fsrc_in_caller : 
  caller:SlicingInternals.fct_slice ->
  to_call:Frama_c_kernel.Kernel_function.t ->
  unit

Source

val call_min_f_in_caller : 
  caller:SlicingInternals.fct_slice ->
  to_call:Frama_c_kernel.Cil_types.kernel_function ->
  unit

Source

val is_already_selected : 
  SlicingInternals.fct_slice ->
  SlicingTypes.sl_select ->
  bool

Source

val add_ff_selection : 
  SlicingInternals.fct_slice ->
  SlicingTypes.sl_select ->
  unit

Sourceval 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.

package frama-c

Module Slicing.SlicingSelectSource

Module `Slicing.SlicingSelect`Source