Module Fct_slice

module Fct_slice: sig .. end
This module deals with slice computation. It computes a mapping between the PDG nodes and some marks (see Fct_slice.FctMarks), and also manage interprocedural propagation (Fct_slice.CallInfo).

Most high level function, named apply_xxx, like apply_change_call, apply_missing_outputs, ..., correspond the actions defined in the specification report.

Many functions are modifying the marks of a slice, so they can return a list of actions to be applied in order to deal with the propagation in the calls and callers.

Moreover, some function (named get_xxx_mark) are provided to retreive the mark of the slice elements.
Raises


val make_new_ff : SlicingInternals.fct_info ->
bool -> SlicingInternals.fct_slice * SlicingInternals.criterion list
build a new empty slice in the given fct_info. If the function has some persistent selection, let's copy it in the new slice. Notice that there can be at most one slice for the application entry point (main), but we allow to have several slice for a library entry point.
Raises SlicingTypes.NoPdg when there is no PDG for the function.

(see new_slice)

build_actions : (bool) is useful if the function has some persistent selection : if the new slice marks will be modified just after that, it is not useful to do examine_calls, but if it is finished, we must generate those actions to choose the calls.
val merge_slices : SlicingInternals.fct_slice ->
SlicingInternals.fct_slice ->
SlicingInternals.fct_slice * SlicingInternals.criterion list
Build a new slice which marks are a join between ff1 marks and ff2 marks. The result ff is not called at the end of this action. examine_calls is called to generate the actions to choose the calls.
val copy_slice : SlicingInternals.fct_slice -> SlicingInternals.fct_slice
val filter_already_in : SlicingInternals.fct_slice ->
SlicingInternals.fct_base_criterion -> SlicingInternals.fct_base_criterion
a function that doesn't modify anything but test if the nodes_marks are already in the slice or not.
Returns the nodes_marks that are not already in.
val apply_add_marks : SlicingInternals.fct_slice ->
SlicingInternals.fct_base_criterion -> SlicingInternals.criterion list
main function to build or modify a slice.
Returns a list of the filters to add to the worklist.
val add_marks_to_fi : SlicingInternals.project ->
SlicingInternals.fct_info ->
SlicingInternals.fct_base_criterion ->
bool ->
SlicingInternals.criterion list -> bool * SlicingInternals.criterion list
add the marks to the persistent marks to be used when new slices will be created. The actions to add the marks to the existing slices are generated in slicingProject. If it is the first persistent selection for this function, and propagate=true, also generates the actions to make every calls to this function visible.
val add_top_mark_to_fi : SlicingInternals.fct_info ->
SlicingInternals.pdg_mark ->
bool -> SlicingInternals.criterion list -> SlicingInternals.criterion list
val check_outputs_before_change_call : SlicingInternals.project ->
SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.fct_slice -> SlicingInternals.criterion list
When the user wants to make a change_call to a function that doesn't compute enough outputs, he can call check_outputs_before_change_call in order to build the action the add those outputs.
val apply_change_call : SlicingInternals.project ->
SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.called_fct -> SlicingInternals.criterion list
check if f_to_call is ok for this call, and if so, change the function call and propagate missing marks in the inputs if needed.
Raises ChangeCallErr if f_to_call doesn't compute enought outputs.
val apply_choose_call : SlicingInternals.project ->
SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.criterion list
Choose the function (slice or source) to call according to the slicing level of the called function. Does nothing if there is already a called function : this is useful because we can sometime generate several choose_call for the same call, and we want to do something only the first time. Build an action change_call to really call it. If the chosen function doesn't compute enough output, build an action to add outputs to it.
val apply_missing_inputs : SlicingInternals.project ->
SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.fct_base_criterion * bool -> SlicingInternals.criterion list
ff calls a slice g that needs more inputs than those computed by ff. The slicing level of ff is used in order to know if we have to modify ff or to call another function.
val apply_missing_outputs : SlicingInternals.project ->
SlicingInternals.fct_slice ->
Cil_types.stmt ->
SlicingInternals.fct_base_criterion ->
bool -> SlicingInternals.criterion list
ff calls a slice g that doesn't compute enough outputs for the call. The missing marks are output_marks. The slicing level has to be used to choose either to modify the called function g or to change it.
val apply_examine_calls : SlicingInternals.fct_slice ->
SlicingInternals.pdg_mark PdgMarks.info_called_outputs ->
SlicingInternals.criterion list
val get_called_slice : SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.fct_slice option * bool
Inform about the called slice or else calls to source functions.
val get_node_mark : SlicingInternals.fct_slice -> PdgTypes.Node.t -> SlicingInternals.pdg_mark
val get_node_key_mark : SlicingInternals.fct_slice -> PdgIndex.Key.t -> SlicingInternals.pdg_mark
val get_top_input_mark : SlicingInternals.fct_info -> SlicingInternals.pdg_mark
val get_stmt_mark : SlicingInternals.fct_slice -> Cil_types.stmt -> SlicingInternals.pdg_mark
val get_label_mark : SlicingInternals.fct_slice ->
Cil_types.stmt -> Cil_types.label -> SlicingInternals.pdg_mark
val get_param_mark : SlicingInternals.fct_slice -> int -> SlicingInternals.pdg_mark
val get_local_var_mark : SlicingInternals.fct_slice -> Cil_types.varinfo -> SlicingInternals.pdg_mark
val get_input_loc_under_mark : SlicingInternals.fct_slice -> Locations.Zone.t -> SlicingInternals.pdg_mark
val get_mark_from_src_fun : SlicingInternals.project -> Kernel_function.t -> SlicingInternals.pdg_mark
The mark m related to all statements of a source function kf. Property : is_bottom (get_from_func proj kf) = not (Project.is_called proj kf)
val merge_inputs_m1_mark : SlicingInternals.fct_slice -> SlicingInternals.pdg_mark
val clear_ff : SlicingInternals.project -> SlicingInternals.fct_slice -> unit
ff has to be removed. We have to check if it is not called and to remove the called function in ff.
Raises SlicingTypes.CantRemoveCalledFf if the slice is called.
val print_ff_sig : Format.formatter -> SlicingInternals.fct_slice -> unit