package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 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
val build_addr_dpds_selection : ?nd_marks:n_or_d_marks -> SlicingTypes.sl_mark -> n_or_d_marks
val build_data_dpds_selection : ?nd_marks:n_or_d_marks -> SlicingTypes.sl_mark -> n_or_d_marks
val build_ctrl_dpds_selection : ?nd_marks:n_or_d_marks -> SlicingTypes.sl_mark -> n_or_d_marks
val build_node_and_dpds_selection : ?nd_marks:n_or_d_marks -> SlicingTypes.sl_mark -> n_or_d_marks
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
val mk_crit_fct_user_select : SlicingInternals.fct_info -> select -> SlicingInternals.criterion
val mk_crit_prop_persit_marks : SlicingInternals.fct_info -> select -> SlicingInternals.criterion
val mk_crit_add_output_marks : SlicingInternals.fct_slice -> select -> SlicingInternals.criterion
val print_nd_and_mark_list : Stdlib.Format.formatter -> n_or_d_marks -> unit

Printing

val print_nodes : Stdlib.Format.formatter -> Pdg_types.PdgTypes.Node.t list -> unit
val print_sel_marks_list : Stdlib.Format.formatter -> select -> unit
val print_crit : Stdlib.Format.formatter -> SlicingInternals.criterion -> unit
val print_f_crit : Stdlib.Format.formatter -> SlicingInternals.fct_user_crit -> unit
val print_list_crit : Stdlib.Format.formatter -> SlicingInternals.criterion list -> unit