Module Slicing.Api.Slice

module Slice: sig .. end

Function slice.


type t 

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

Used to get an empty slice (nothing selected) related to a function.

val remove : t -> unit

Remove the slice from the project. The slice shouldn't be called.

val remove_uncalled : unit -> unit

Remove the uncalled slice from the project.

Getters

val get_all : Cil_types.kernel_function -> t list

Get all slices related to a function.

val get_function : t -> Cil_types.kernel_function

To get the function related to a slice

val get_callers : t -> t list

Get the slices having direct calls to a slice.

val get_called_slice : t -> Cil_types.stmt -> t option

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

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 -> Slicing.Api.Mark.t

Get the mark value of a statement.

val get_mark_from_label : t ->
Cil_types.stmt -> Cil_types.label -> Slicing.Api.Mark.t

Get the mark value of a label.

val get_mark_from_local_var : t -> Cil_types.varinfo -> Slicing.Api.Mark.t

Get the mark value of local variable.

val get_mark_from_formal : t -> Cil_types.varinfo -> Slicing.Api.Mark.t

Get the mark from the formal of a function.

val get_user_mark_from_inputs : t -> Slicing.Api.Mark.t

Get a mark that is the merged user inputs marks of the slice

Not for casual users

val get_num_id : t -> int
val from_num_id : Cil_types.kernel_function -> int -> t
val pretty : Stdlib.Format.formatter -> t -> unit

May be used for debugging... Pretty print slice information.