Module `Slicing.SlicingActions`Source

Sourcetype select = SlicingTypes.sl_mark Pdg_types.PdgMarks.select

Sourcetype n_or_d_marks

selection mode (ie which mark to associate to the node and how to propagate in the different kinds of dependencies)

val build_simple_node_selection : 
  ?nd_marks:n_or_d_marks ->
  SlicingTypes.sl_mark ->
  n_or_d_marks

Source

val build_addr_dpds_selection : 
  ?nd_marks:n_or_d_marks ->
  SlicingTypes.sl_mark ->
  n_or_d_marks

Source

val build_data_dpds_selection : 
  ?nd_marks:n_or_d_marks ->
  SlicingTypes.sl_mark ->
  n_or_d_marks

Source

val build_ctrl_dpds_selection : 
  ?nd_marks:n_or_d_marks ->
  SlicingTypes.sl_mark ->
  n_or_d_marks

Source

val build_node_and_dpds_selection : 
  ?nd_marks:n_or_d_marks ->
  SlicingTypes.sl_mark ->
  n_or_d_marks

Source

val translate_crit_to_select : 
  Pdg.Api.t ->
  ?to_select:select ->
  ((Pdg_types.PdgTypes.Node.t * Frama_c_kernel.Locations.Zone.t option) list
   * n_or_d_marks)
    list ->
  select

Source

val mk_fct_crit : 
  SlicingInternals.fct_info ->
  SlicingInternals.fct_crit ->
  SlicingInternals.criterion

Source

val mk_crit_fct_user_select : 
  SlicingInternals.fct_info ->
  select ->
  SlicingInternals.criterion

Source

val mk_crit_fct_top : 
  SlicingInternals.fct_info ->
  SlicingTypes.sl_mark ->
  SlicingInternals.criterion

Source

val mk_crit_prop_persit_marks : 
  SlicingInternals.fct_info ->
  select ->
  SlicingInternals.criterion

Source

val mk_ff_user_select : 
  SlicingInternals.fct_slice ->
  select ->
  SlicingInternals.criterion

Source

val mk_crit_choose_call : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  SlicingInternals.criterion

Source

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

Source

val mk_crit_missing_inputs : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  (select * bool) ->
  SlicingInternals.criterion

Source

val mk_crit_missing_outputs : 
  SlicingInternals.fct_slice ->
  Frama_c_kernel.Cil_types.stmt ->
  (select * bool) ->
  SlicingInternals.criterion

Source

val mk_crit_examines_calls : 
  SlicingInternals.fct_slice ->
  SlicingTypes.sl_mark Pdg_types.PdgMarks.info_called_outputs ->
  SlicingInternals.criterion

Source

val mk_appli_select_calls : 
  SlicingInternals.fct_info ->
  SlicingInternals.criterion

Source

val mk_crit_mark_calls : 
  SlicingInternals.fct_info ->
  Frama_c_kernel.Cil_types.kernel_function ->
  SlicingTypes.sl_mark ->
  SlicingInternals.criterion

Source

val mk_crit_add_output_marks : 
  SlicingInternals.fct_slice ->
  select ->
  SlicingInternals.criterion

Sourceval print_nd_and_mark_list : Stdlib.Format.formatter -> n_or_d_marks -> unit

Printing

Source

val print_nodes : 
  Stdlib.Format.formatter ->
  Pdg_types.PdgTypes.Node.t list ->
  unit

Sourceval print_sel_marks_list : Stdlib.Format.formatter -> select -> unit

Sourceval print_crit : Stdlib.Format.formatter -> SlicingInternals.criterion -> unit

Source

val print_f_crit : 
  Stdlib.Format.formatter ->
  SlicingInternals.fct_user_crit ->
  unit

Source

val print_list_crit : 
  Stdlib.Format.formatter ->
  SlicingInternals.criterion list ->
  unit

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Slicing.SlicingActions`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Slicing.SlicingActionsSource

Module `Slicing.SlicingActions`Source