Module SlicingCmds

module SlicingCmds: sig .. end

Those functions were previously outside the slicing module to show how to use the slicing API. So, they are supposed to use the slicing module through Db.Slicing only. There are mainly high level functions which make easier to achieve simple tasks.

type set = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t

val get_select_kf : SlicingTypes.sl_select -> Cil_types.kernel_function

val topologic_propagation : unit -> unit

Topologically propagate user marks to callers in whole project

val select_pdg_nodes : set ->
       SlicingTypes.sl_mark ->
       PdgTypes.Node.t list -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add a selection of the pdg nodes.

val select_stmt : set ->
       spare:bool -> Cil_types.stmt -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add a selection of the statement.

val select_func_calls_to : set -> spare:bool -> Kernel_function.t -> set

Registered as a slicing selection function: Add a selection of calls to a kf.

val select_func_calls_into : set -> spare:bool -> Kernel_function.t -> set

Registered as a slicing selection function: Add a selection of calls to a kf.

val select_func_zone : set ->
       SlicingTypes.sl_mark ->
       Locations.Zone.t -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add selection of function outputs.

val select_func_return : set -> spare:bool -> Kernel_function.t -> set

Registered as a slicing selection function: Add a selection of the kf return statement.

val select_stmt_ctrl : set ->
       spare:bool -> Cil_types.stmt -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add a selection of the statement reachability. Note: add also a transparent selection on the whole statement.

val select_stmt_zone : set ->
       SlicingTypes.sl_mark ->
       Locations.Zone.t ->
       before:bool -> Cil_types.stmt -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add a selection of data relative to a statement. Note: add also a transparent selection on the whole statement.

val select_stmt_lval : set ->
       SlicingTypes.sl_mark ->
       Datatype.String.Set.t ->
       before:bool ->
       Cil_types.stmt ->
       eval:Cil_types.stmt -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add a selection of data relative to a statement. Variables of lval_str string are bounded relatively to the whole scope of the function kf. The interpretation of the address of the lvalues is done just before the execution of the statement ~eval. The selection preserve the value of these lvalues before or after (c.f. boolean ~before) the statement ki. Note: add also a transparent selection on the whole statement.

val select_stmt_lval_rw : set ->
       SlicingTypes.sl_mark ->
       rd:Datatype.String.Set.t ->
       wr:Datatype.String.Set.t ->
       Cil_types.stmt -> eval:Cil_types.stmt -> Kernel_function.t -> set

Registered as a slicing selection function: Add a selection of rw accesses to lvalues relative to a statement. Variables of ~rd and ~wr string are bounded relatively to the whole scope of the function kf. The interpretation of the address of the lvalues is done just before the execution of the statement ~eval. The selection preserve the ~rd and ~wr accesses directly contained into the statement ki. i.e. when ki is a call, the selection doesn't look at the assigns clause of the called function. Note: add also a transparent selection on the whole statement.

val select_stmt_pred : set ->
       SlicingTypes.sl_mark ->
       Cil_types.predicate ->
       Cil_types.stmt -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add selection of the annotations related to a statement. Note: add also a transparent selection on the whole statement.

val select_stmt_term : set ->
       SlicingTypes.sl_mark ->
       Cil_types.term ->
       Cil_types.stmt -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add selection of the annotations related to a statement. Note: add also a transparent selection on the whole statement.

val select_stmt_annot : set ->
       SlicingTypes.sl_mark ->
       spare:bool ->
       Cil_types.code_annotation ->
       Cil_types.stmt -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add selection of the annotations related to a statement. Note: add also a transparent selection on the whole statement.

val select_stmt_annots : set ->
       SlicingTypes.sl_mark ->
       spare:bool ->
       threat:bool ->
       user_assert:bool ->
       slicing_pragma:bool ->
       loop_inv:bool ->
       loop_var:bool ->
       Cil_types.stmt -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add selection of the annotations related to a statement. Note: add also a transparent selection on the whole statement.

val select_func_annots : set ->
       SlicingTypes.sl_mark ->
       spare:bool ->
       threat:bool ->
       user_assert:bool ->
       slicing_pragma:bool ->
       loop_inv:bool ->
       loop_var:bool -> Cil_types.kernel_function -> set

Registered as a slicing selection function: Add a selection of the annotations related to a function.

val select_func_lval : set ->
       SlicingTypes.sl_mark ->
       Datatype.String.Set.t -> Kernel_function.t -> set

Registered as a slicing selection function: Add selection of function outputs. Variables of lval_str string are bounded relatively to the whole scope of the function kf. The interpretation of the address of the lvalues is done just before the execution of the first statement kf. The selection preserve the value of these lvalues before execution of the return statement.

val select_func_lval_rw : set ->
       SlicingTypes.sl_mark ->
       rd:Datatype.String.Set.t ->
       wr:Datatype.String.Set.t ->
       eval:Cil_types.stmt -> Kernel_function.t -> set

Registered as a slicing selection function: Add a selection of data relative to read/write accesses. Interpret the ~rd lvalues and the ~wr lvalues from ~eval statements of kf:

Variables of lval_str string are bounded relatively to the whole scope of the function kf.
The interpretation of the address of the lvalues is done just before the execution of the statement ~eval. Find read/write accesses from the whole project if ki_opt=None.

val add_selection : set -> unit

Registered as a slicing request function: Add selections to all concerned slices, as slicing requests and apply them, kernel function by kernel function. Note:

the function begins by applying the remaining internal requests.
the requests added for the last kernel function are not applied.

val add_persistent_selection : set -> unit

Registered as a slicing request function: Add selections that will be applied to all the slices of the function (already existing or created later) Note:

the function begins by applying the remaining internal requests.
the requests added for the last kernel function are not applied.

val add_persistent_cmdline : unit -> unit

Registered as a slicing request function: Add selections that will be applied to all the slices of the function (already existing or created later) Note:

the function begins by applying the remaining internal requests.
the requests added for the last kernel function are not applied.

val apply_all : propagate_to_callers:bool -> unit

val apply_all_actions : unit -> unit

val apply_next_action : unit -> unit