Slicing.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.
* These types are the only one that should be used by the API functions. * Public type definitions should be hidden to the outside world, * but it is not really possible to have abstract types since Slicing has to * use Db.Slicing functions... So, it is up to the user of this module to use * only this public part.
type sl_project = SlicingInternals.project
contains global things that has been computed so far for the slicing project. This includes :
type sl_select =
Frama_c_kernel.Cil_types.varinfo * SlicingInternals.fct_user_crit
Type 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_crit
type sl_fct_slice = SlicingInternals.fct_slice
Function slice
type sl_mark = SlicingInternals.pdg_mark
Marks : used to put 'colors' in the result
val pp_sl_project :
Frama_c_kernel.Type.precedence ->
Stdlib.Format.formatter ->
'a ->
unit
module Sl_project : Frama_c_kernel.Datatype.S with type t = sl_project
module Sl_select : Frama_c_kernel.Datatype.S with type t = sl_select
val pp_sl_fct_slice :
Frama_c_kernel.Type.precedence ->
Stdlib.Format.formatter ->
SlicingInternals.fct_slice ->
unit
module Sl_fct_slice :
Frama_c_kernel.Datatype.S with type t = SlicingInternals.fct_slice
val dyn_sl_fct_slice : Sl_fct_slice.t Frama_c_kernel.Type.t
module Sl_mark :
Frama_c_kernel.Datatype.S_with_collections
with type t = SlicingInternals.pdg_mark
val dyn_sl_mark : Sl_mark.t Frama_c_kernel.Type.t