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.
Returns the newly created slices.
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.