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_to : Db.Slicing.Select.set ->
spare:bool -> Cil_types.kernel_function -> 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 -> Cil_types.kernel_function -> 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
:
- 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
.
Find read/write accesses from the whole project if ki_opt
=None.
Otherwise, restrict the research among the direct effect of ki_opt
statement.
i.e. when ki_opt
is a call, the selection doesn't look at the assigns clause
of a call.
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
:
- 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
.
Find read/write accesses from the whole project if ki_opt
=None.
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:
- 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.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:
- the function begins by applying the remaining internal requests.
- the requests added for the last kernel function are not applied.
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:
- the function begins by applying the remaining internal requests.
- the requests added for the last kernel function are not applied.
val apply_all : Db.Slicing.Project.t -> propagate_to_callers:bool -> unit