Frama-C API - SlicingTypes
Slicing module types.
raised when someone tries to build more than one slice for the entry point.
raised when one tries to select something in a function where we are not able to compute the Pdg.
Public types
These types are the only one that should be used by the API functions. Public type definitions should be hidden to the outside world.
type sl_project = SlicingInternals.projectcontains global things that has been computed so far for the slicing project. This includes :
- the slices of the functions,
- and the queue of actions to be applied.
type sl_select = Frama_c_kernel.Cil_types.varinfo * SlicingInternals.fct_user_critType of the selections (we store the varinfo because we cannot use the kernel_function in this file)
module Fct_user_crit : Frama_c_kernel.Datatype.S with type t = SlicingInternals.fct_user_crittype sl_fct_slice = SlicingInternals.fct_sliceFunction slice
type sl_mark = SlicingInternals.pdg_markMarks : used to put 'colors' in the result
val pp_sl_project : Frama_c_kernel.Type.precedence -> Stdlib.Format.formatter -> 'a -> unitmodule Sl_project : Frama_c_kernel.Datatype.S with type t = sl_projectmodule Sl_select : Frama_c_kernel.Datatype.S with type t = sl_selectval pp_sl_fct_slice : Frama_c_kernel.Type.precedence -> Stdlib.Format.formatter -> SlicingInternals.fct_slice -> unitmodule Sl_fct_slice : Frama_c_kernel.Datatype.S with type t = SlicingInternals.fct_sliceval dyn_sl_fct_slice : Sl_fct_slice.t Frama_c_kernel.Type.tmodule Sl_mark : Frama_c_kernel.Datatype.S_with_collections with type t = SlicingInternals.pdg_markval dyn_sl_mark : Sl_mark.t Frama_c_kernel.Type.t