Module `Slicing.Fct_slice`Source

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

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

Source

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

Sourceval copy_slice : SlicingInternals.fct_slice -> SlicingInternals.fct_slice

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Sourceval get_top_input_mark : SlicingInternals.fct_info -> SlicingInternals.pdg_mark

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

val merge_inputs_m1_mark : 
  SlicingInternals.fct_slice ->
  SlicingInternals.pdg_mark

Sourceval clear_ff : SlicingInternals.fct_slice -> unit

Sourceval print_ff_sig : Format.formatter -> SlicingInternals.fct_slice -> unit

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/frama-c-slicing.core/Slicing/Fct_slice/index.html

Module `Slicing.Fct_slice`Source

package frama-c

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/frama-c-slicing.core/Slicing/Fct_slice/index.html

Module Slicing.Fct_sliceSource

dune-project
Dependency

Module `Slicing.Fct_slice`Source