Module SlicingTypes

module SlicingTypes: sig .. end

Slicing module types.

Slicing module types.


exception Slicing_Internal_Error of string
exception ChangeCallErr of string
exception PtrCallExpr
exception CantRemoveCalledFf
exception WrongSlicingLevel
exception OnlyOneEntryPointSlice

raised when someone tries to build more than one slice for the entry point.

raised when someone tries to build more than one slice for the entry point.

exception NoPdg

raised when one tries to select something in a function where we are not able to compute the Pdg.

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, 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 :

contains global things that has been computed so far for the slicing project. This includes :

type sl_select = 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)

Type of the selections (we store the varinfo because we cannot use the kernel_function in this file)

module Fct_user_crit: Datatype.S  with type t = SlicingInternals.fct_user_crit
type sl_fct_slice = SlicingInternals.fct_slice 

Function slice

Function slice

type sl_mark = SlicingInternals.pdg_mark 

Marks : used to put 'colors' in the result

Marks : used to put 'colors' in the result

For the journalization of values of these types

val pp_sl_project : Type.precedence -> Stdlib.Format.formatter -> 'a -> unit
module Sl_project: Datatype.S  with type t = sl_project
module Sl_select: Datatype.S  with type t = sl_select
val pp_sl_fct_slice : Type.precedence ->
Stdlib.Format.formatter -> SlicingInternals.fct_slice -> unit
module Sl_fct_slice: Datatype.S  with type t = SlicingInternals.fct_slice
val dyn_sl_fct_slice : Sl_fct_slice.t Type.t
val pp_sl_mark : Type.precedence ->
Stdlib.Format.formatter -> SlicingInternals.pdg_mark -> unit
module Sl_mark: Datatype.S_with_collections  with
  type t = SlicingInternals.pdg_mark
val dyn_sl_mark : Sl_mark.t Type.t