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.
val topologic_propagation : unit -> unit
Topologically propagate user marks to callers in whole project
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_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_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_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 outputs.
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 ->
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 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 : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
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 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 : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
Cil_types.predicate ->
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 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 : Db.Slicing.Select.set ->
Db.Slicing.Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
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
~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 : 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:
- the function begins by applying the remaining internal requests.
- the requests added for the last kernel function are not applied.
val add_persistent_selection : 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:
- 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