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.