Module Slicing.Api.Request

module Request: sig .. end

Requests for slicing jobs. Slicing requests are part of a slicing project. So, user requests affect slicing project.


Applying the added requests

val apply_all : propagate_to_callers:bool -> unit

Apply all slicing requests.

Adding 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.

Not for casual users and not journalized

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.