module Request:sig
..end
Requests for slicing jobs. Slicing requests are part of a slicing project. So, user requests affect slicing project.
val apply_all : propagate_to_callers:bool -> unit
Apply all slicing requests.
val add_selection : Slicing.Api.Select.set -> unit
Add a selection request to all (existing) slices of a function to the project requests.
val add_persistent_selection : Slicing.Api.Select.set -> unit
Add a persistent selection request to all slices (already existing or created later) of a function to the project requests.
val add_persistent_cmdline : unit -> unit
Add persistent selection from the command line.
val add_slice_selection_internal : Slicing.Api.Slice.t -> Slicing.Api.Select.t -> unit
May be used to add a selection request for a function slice to the project requests.
val add_selection_internal : Slicing.Api.Select.t -> unit
May be used to add a selection request to the project requests. This selection will be applied to every slicies of the function (already existing or created later).
val add_call_slice : caller:Slicing.Api.Slice.t -> to_call:Slicing.Api.Slice.t -> unit
May be used to change every call to any to_call
source or specialisation in order
to call to_call
in caller
.
val add_call_fun : caller:Slicing.Api.Slice.t -> to_call:Cil_types.kernel_function -> unit
May be used to change every call to any to_call
source or specialisation
in order to call the source function to_call
in caller
.
val add_call_min_fun : caller:Slicing.Api.Slice.t -> to_call:Cil_types.kernel_function -> unit
May be used to change each call to to_call
in caller
such that, at least, it
will be visible at the end, ie. call either the source function or
one of to_call
slice (depending on the slicing_level
).
val is_request_empty_internal : unit -> bool
May be used to know if internal requests are pending.
Return true when the requested selection is already selected into the slice.
val apply_all_internal : unit -> unit
May be used to apply all slicing requests.
val apply_next_internal : unit -> unit
May be used to apply the first slicing request of the project list and remove it from the list. That may modify the contents of the remaining list. For example, new requests may be added to the list.
val merge_slices : Slicing.Api.Slice.t ->
Slicing.Api.Slice.t -> replace:bool -> Slicing.Api.Slice.t
May be used to build a new slice which marks is a merge of the two given slices.
choose_call
requests are added to the project in order to choose
the called functions for this new slice.
If replace
is true, more requests are added to call this new
slice instead of the two original slices. When these requests will
be applied, the user will be able to remove those two slices using
Db.Slicing.Slice.remove
.
val copy_slice : Slicing.Api.Slice.t -> Slicing.Api.Slice.t
May be used to copy the input slice. The new slice is not called, so it is the user responsibility to change the calls if he wants to.
val split_slice : Slicing.Api.Slice.t -> Slicing.Api.Slice.t list
May be used to copy the input slice to have one slice for each call of the original slice and generate requests in order to call them.
val propagate_user_marks : unit -> unit
May be used to apply pending request then propagate user marks to callers recursively then apply pending requests
val pretty : Format.formatter -> unit
May be used for debugging... Pretty print the request list.