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.

module Kinstr: sig .. end
Utilities for kinstr.
val topologic_propagation : Db.Slicing.Project.t -> unit
Topologically propagate user marks to callers in whole project
val add_to_selection : Db.Slicing.Select.set -> Db.Slicing.Select.t -> Db.Slicing.Select.set
val select_pdg_nodes : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
PdgTypes.Node.t list -> Cil_types.kernel_function -> Db.Slicing.Select.set
Registered as a slicing selection function: Add a selection of the pdg nodes.
val select_stmt : Db.Slicing.Select.set ->
spare:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.set
Registered as a slicing selection function: Add a selection of the statement.
val select_entry_point_and_some_inputs_outputs : Db.Slicing.Select.set ->
mark:Db.Slicing.Mark.t ->
Kernel_function.t ->
return:bool ->
outputs:Locations.Zone.t -> inputs:Locations.Zone.t -> Db.Slicing.Select.set
Add a selection to the entrance of the function kf and add a selection to its return if ~return is true and add a selection to ~inputs parts of its inputs and add a selection to ~ouputs parts of its outputs
val generic_select_func_calls : ('a -> spare:'b -> Cil_types.stmt -> Cil_types.kernel_function -> 'a) ->
'a -> spare:'b -> Cil_types.kernel_function -> 'a
val select_func_calls_into : Db.Slicing.Select.set ->
spare:bool -> Kernel_function.t -> Db.Slicing.Select.set
Registered as a slicing selection function: Add a selection of calls to a kf.
val select_func_calls_to : Db.Slicing.Select.set ->
spare:bool -> Kernel_function.t -> Db.Slicing.Select.set
Registered as a slicing selection function: Add a selection of calls to a kf.
val select_func_zone : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Locations.Zone.t -> Cil_types.kernel_function -> Db.Slicing.Select.set
Registered as a slicing selection function: Add selection of function ouputs.
val select_func_return : Db.Slicing.Select.set ->
spare:bool -> Kernel_function.t -> Db.Slicing.Select.set
Registered as a slicing selection function: Add a selection of the kf return statement.
val select_stmt_ctrl : Db.Slicing.Select.set ->
spare:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.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 : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Locations.Zone.t ->
before:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.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 : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Datatype.String.Set.t ->
before:bool ->
Cil_types.stmt ->
scope:Cil_types.stmt ->
eval:Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.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 scope of the statement ~scope. 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_lval_rw : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
scope:Cil_types.stmt ->
eval:Cil_types.stmt ->
Kernel_function.t -> Cil_types.stmt option -> Db.Slicing.Select.set
Add a selection of data relative to read/write accesses. Interpret the ~rd lvalues and the ~wr lvalues from ~scope, ~eval statements of kf:
val select_stmt_lval_rw : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
Cil_types.stmt ->
scope:Cil_types.stmt ->
eval:Cil_types.stmt -> Kernel_function.t -> Db.Slicing.Select.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 scope of the statement ~scope. 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_decl_var : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Cil_types.varinfo -> Cil_types.kernel_function -> Db.Slicing.Select.set
Add a selection of the declaration of vi.
val select_ZoneAnnot_pragmas : Db.Slicing.Select.set ->
spare:bool ->
Db.Properties.Interp.To_zone.t_pragmas ->
Cil_types.kernel_function -> Db.Slicing.Select.set
val select_ZoneAnnot_zones_decl_vars : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Db.Properties.Interp.To_zone.t list * Db.Properties.Interp.To_zone.t_decl ->
Cil_types.kernel_function -> Db.Slicing.Select.set
val get_or_raise : 'a option * 'b -> 'a * 'b
val select_stmt_pred : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Cil_types.predicate Cil_types.named ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.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 : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Cil_types.term ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.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 : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
spare:bool ->
Cil_types.code_annotation ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.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 : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
spare:bool ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool ->
loop_var:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> Db.Slicing.Select.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 : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
spare:bool ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool ->
loop_var:bool -> Cil_types.kernel_function -> Db.Slicing.Select.set
Registered as a slicing selection function: Add a selection of the annotations related to a function.
val select_func_lval : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Datatype.String.Set.t -> Kernel_function.t -> Db.Slicing.Select.set
Registered as a slicing selection function: Add selection of function ouputs. Variables of lval_str string are bounded relatively to the scope of the first statement of 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 : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
scope:Cil_types.stmt ->
eval:Cil_types.stmt -> Kernel_function.t -> Db.Slicing.Select.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 ~scope, ~eval statements of kf:
val add_selection : Db.Slicing.Project.t -> Db.Slicing.Select.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:
val add_persistent_selection : Db.Slicing.Project.t -> Db.Slicing.Select.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:
val add_persistent_cmdline : Db.Slicing.Project.t -> 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:
val apply_all : Db.Slicing.Project.t -> propagate_to_callers:bool -> unit