Module Db.Slicing.Request

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) Pervasives.ref
Apply all slicing requests.

Adding a request


val add_selection : (Db.Slicing.Select.set -> unit) Pervasives.ref
Add a selection request to all slices (existing) of a function to the project requests.
val add_persistent_selection : (Db.Slicing.Select.set -> unit) Pervasives.ref
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) Pervasives.ref
Add persistent selection from the command line.
val is_already_selected_internal : (Db.Slicing.Slice.t -> Db.Slicing.Select.t -> bool) Pervasives.ref
Return true when the requested selection is already selected into the slice.
val add_slice_selection_internal : (Db.Slicing.Slice.t -> Db.Slicing.Select.t -> unit) Pervasives.ref
Internally used to add a selection request for a function slice to the project requests.
val add_selection_internal : (Db.Slicing.Select.t -> unit) Pervasives.ref
Internally 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:Db.Slicing.Slice.t -> to_call:Db.Slicing.Slice.t -> unit)
Pervasives.ref
change every call to any to_call source or specialisation in order to call to_call in caller.
val add_call_fun : (caller:Db.Slicing.Slice.t -> to_call:Cil_types.kernel_function -> unit)
Pervasives.ref
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:Db.Slicing.Slice.t -> to_call:Cil_types.kernel_function -> unit)
Pervasives.ref
For each call to to_call in caller such so 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).

Internal use only


val apply_all_internal : (unit -> unit) Pervasives.ref
Internally used to apply all slicing requests.
val apply_next_internal : (unit -> unit) Pervasives.ref
Internally 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 is_request_empty_internal : (unit -> bool) Pervasives.ref
Internally used to know if internal requests are pending.
val merge_slices : (Db.Slicing.Slice.t ->
Db.Slicing.Slice.t -> replace:bool -> Db.Slicing.Slice.t)
Pervasives.ref
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 : (Db.Slicing.Slice.t -> Db.Slicing.Slice.t) Pervasives.ref
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 : (Db.Slicing.Slice.t -> Db.Slicing.Slice.t list) Pervasives.ref
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) Pervasives.ref
Apply pending request then propagate user marks to callers recursively then apply pending requests
val pretty : (Format.formatter -> unit) Pervasives.ref
For debugging... Pretty print the request list.