Fct_slice (frama-c-slicing.Slicing.Fct

val is_src_fun_called : Frama_c_kernel.Cil_types.kernel_function -> bool

Return true if the source function is called (even indirectly via transitivity) from a Slice.t.

val is_src_fun_visible : Frama_c_kernel.Cil_types.kernel_function -> bool

Return true if the source function is visible (even indirectly via transitivity) from a Slice.t.

val make_new_ff : 
  SlicingInternals.fct_info ->
  bool ->
  SlicingInternals.fct_slice * SlicingInternals.criterion list

raises SlicingTypes.ExternalFunction
if the function has no source code, because there cannot be any slice for it.

raises SlicingTypes.NoPdg
when there is no PDG for the function.

val merge_slices : 
  SlicingInternals.fct_slice ->
  SlicingInternals.fct_slice ->
  SlicingInternals.fct_slice * SlicingInternals.criterion list

val copy_slice : SlicingInternals.fct_slice -> SlicingInternals.fct_slice

val filter_already_in : 
  SlicingInternals.fct_slice ->
  SlicingInternals.fct_base_criterion ->
  SlicingInternals.fct_base_criterion

val apply_add_marks : 
  SlicingInternals.fct_slice ->
  SlicingInternals.fct_base_criterion ->
  SlicingInternals.criterion list

val add_marks_to_fi : 
  SlicingInternals.fct_info ->
  SlicingInternals.fct_base_criterion ->
  bool ->
  SlicingInternals.criterion list ->
  bool * SlicingInternals.criterion list

val add_top_mark_to_fi : 
  SlicingInternals.fct_info ->
  SlicingInternals.pdg_mark ->
  bool ->
  SlicingInternals.criterion list ->
  SlicingInternals.criterion list

val check_outputs_before_change_call : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  SlicingInternals.fct_slice ->
  SlicingInternals.criterion list

val apply_change_call : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  SlicingInternals.called_fct ->
  SlicingInternals.criterion list

val apply_choose_call : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  SlicingInternals.criterion list

val apply_missing_inputs : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  (SlicingInternals.fct_base_criterion * bool) ->
  SlicingInternals.criterion list

val apply_missing_outputs : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  SlicingInternals.fct_base_criterion ->
  bool ->
  SlicingInternals.criterion list

val apply_examine_calls : 
  SlicingInternals.fct_slice ->
  SlicingInternals.pdg_mark Pdg_types.PdgMarks.info_called_outputs ->
  SlicingInternals.criterion list

val get_called_slice : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  SlicingInternals.fct_slice option * bool

val get_node_mark : 
  SlicingInternals.fct_slice ->
  Pdg_types.PdgTypes.Node.t ->
  SlicingInternals.pdg_mark

val get_node_key_mark : 
  SlicingInternals.fct_slice ->
  Pdg_types.PdgIndex.Key.t ->
  SlicingInternals.pdg_mark

val get_top_input_mark : SlicingInternals.fct_info -> SlicingInternals.pdg_mark

val get_stmt_mark : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  SlicingInternals.pdg_mark

val get_label_mark : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.label ->
  SlicingInternals.pdg_mark

val get_param_mark : 
  SlicingInternals.fct_slice ->
  int ->
  SlicingInternals.pdg_mark

val get_local_var_mark : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.varinfo ->
  SlicingInternals.pdg_mark

val get_input_loc_under_mark : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Locations.Zone.t ->
  SlicingInternals.pdg_mark

val get_mark_from_src_fun : 
  Frama_c_kernel.Kernel_function.t ->
  SlicingInternals.pdg_mark

val merge_inputs_m1_mark : 
  SlicingInternals.fct_slice ->
  SlicingInternals.pdg_mark

val clear_ff : SlicingInternals.fct_slice -> unit

val print_ff_sig : 
  Stdlib.Format.formatter ->
  SlicingInternals.fct_slice ->
  unit