Module Db.Slicing.Slice

module Slice: sig .. end
Function slice.

type t = SlicingTypes.sl_fct_slice 
Abstract data type for function slice.
val dyn_t : t Type.t
For dynamic type checking and journalization.
val create : (Cil_types.kernel_function -> t) Pervasives.ref
Used to get an empty slice (nothing selected) related to a function.
val remove : (t -> unit) Pervasives.ref
Remove the slice from the project. The slice shouldn't be called.
val remove_uncalled : (unit -> unit) Pervasives.ref
Remove the uncalled slice from the project.

Getters


val get_all : (Cil_types.kernel_function -> t list) Pervasives.ref
Get all slices related to a function.
val get_function : (t -> Cil_types.kernel_function) Pervasives.ref
To get the function related to a slice
val get_callers : (t -> t list) Pervasives.ref
Get the slices having direct calls to a slice.
val get_called_slice : (t -> Cil_types.stmt -> t option)
Pervasives.ref
To get the slice directly called by the statement of a slice. Returns None when the statement mark is bottom, or else the statement isn't a call or else the statement is a call to one or several (via pointer) source functions.
val get_called_funcs : (t -> Cil_types.stmt -> Cil_types.kernel_function list)
Pervasives.ref
To get the source functions called by the statement of a slice. Returns an empty list when the statement mark is bottom, or else the statement isn't a call or else the statement is a call to a function slice.
val get_mark_from_stmt : (t -> Cil_types.stmt -> Db.Slicing.Mark.t) Pervasives.ref
Get the mark value of a statement.
val get_mark_from_label : (t -> Cil_types.stmt -> Cil_types.label -> Db.Slicing.Mark.t)
Pervasives.ref
Get the mark value of a label.
val get_mark_from_local_var : (t -> Cil_types.varinfo -> Db.Slicing.Mark.t) Pervasives.ref
Get the mark value of local variable.
val get_mark_from_formal : (t -> Cil_types.varinfo -> Db.Slicing.Mark.t) Pervasives.ref
Get the mark from the formal of a function.
val get_user_mark_from_inputs : (t -> Db.Slicing.Mark.t) Pervasives.ref
Get a mark that is the merged user inputs marks of the slice

Internal use only


val get_num_id : (t -> int) Pervasives.ref
val from_num_id : (Cil_types.kernel_function -> int -> t) Pervasives.ref
val pretty : (Format.formatter -> t -> unit) Pervasives.ref
For debugging... Pretty print slice information.