Module SlicingTypes

module SlicingTypes: sig .. end

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.

exception NoPdg

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 :

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)

module Fct_user_crit: Datatype.Make(sig
include Datatype.Undefined
type t = SlicingInternals.fct_user_crit 
val reprs : SlicingInternals.fct_user_crit list
val name : string
val mem_project : (Project_skeleton.t -> bool) -> 'a -> bool
val varname : 'a -> string
end)
type sl_fct_slice = SlicingInternals.fct_slice 

Function slice

type sl_mark = SlicingInternals.pdg_mark 

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.Make(sig
include Datatype.Undefined
type t = SlicingTypes.sl_project 
val reprs : SlicingInternals.project list
val name : string
val internal_pretty_code : Type.precedence -> Stdlib.Format.formatter -> 'a -> unit
val varname : 'a -> string
val mem_project : (Project_skeleton.t -> bool) -> 'a -> bool
end)
module Sl_select: Datatype.Make(sig
include Datatype.Undefined
type t = SlicingTypes.sl_select 
val reprs : (Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit) list
val name : string
val varname : 'a -> string
val mem_project : (Project_skeleton.t -> bool) -> 'a -> bool
end)
val pp_sl_fct_slice : Type.precedence ->
Stdlib.Format.formatter -> SlicingInternals.fct_slice -> unit
module Sl_fct_slice: Datatype.Make(sig
include Datatype.Undefined
type t = SlicingInternals.fct_slice 
val name : string
val reprs : SlicingInternals.fct_slice list
val internal_pretty_code : Type.precedence ->
Stdlib.Format.formatter -> SlicingInternals.fct_slice -> unit
val mem_project : (Project_skeleton.t -> bool) -> 'a -> bool
end)
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.Make_with_collections(sig
type t = SlicingInternals.pdg_mark 
val name : string
val structural_descr : Structural_descr.t
val reprs : SlicingInternals.pdg_mark list
val compare : SlicingInternals.pdg_mark -> SlicingInternals.pdg_mark -> int
val equal : t -> t -> bool
val hash : 'a -> int
val copy : 'a -> 'b
val rehash : 'a -> 'b
val internal_pretty_code : Type.precedence ->
Stdlib.Format.formatter -> SlicingInternals.pdg_mark -> unit
val pretty : Stdlib.Format.formatter -> 'a -> unit
val mem_project : (Project_skeleton.t -> bool) -> 'a -> bool
val varname : 'a -> 'b
end)
val dyn_sl_mark : Sl_mark.t Type.t