module Select:sig
..end
Slicing selections.
type
t
Internal selection.
val dyn_t : t Type.t
For dynamic type checking and journalization.
type
set
Set of colored selections.
val dyn_set : set Type.t
For dynamic type checking and journalization.
val empty_selects : set
Empty selection.
val select_stmt : set ->
spare:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> set
To select a statement.
val select_stmt_ctrl : set ->
spare:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> set
To select a statement reachability. Note: add also a transparent selection on the whole statement.
val select_stmt_lval_rw : set ->
Slicing.Api.Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
Cil_types.stmt ->
eval:Cil_types.stmt -> Cil_types.kernel_function -> set
To select rw accesses to lvalues (given as a string) related to a
statement.
Variable names used in the sets of strings ~rd
and ~wr
are relative
to the function scope.
The interpretation of the address of the lvalues is
done just before the execution of the statement ~eval
.
The selection preserves the ~rd
and ~wr
accesses contained into
the statement ki
.
Note: add also a transparent selection on the whole statement.
~scope
removed.val select_stmt_lval : set ->
Slicing.Api.Mark.t ->
Datatype.String.Set.t ->
before:bool ->
Cil_types.stmt ->
eval:Cil_types.stmt -> Cil_types.kernel_function -> set
To select lvalues (given as string) related to a statement.
Variable names used in the sets of strings ~rd
and ~wr
are relative
to the function scope.
The interpretation of the address of the lvalue 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.
~scope
removed.val select_stmt_annots : set ->
Slicing.Api.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 -> set
To select the annotations related to a statement. Note: add also a transparent selection on the whole statement.
val select_func_lval_rw : set ->
Slicing.Api.Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
eval:Cil_types.stmt -> Cil_types.kernel_function -> set
To select rw accesses to lvalues (given as a string) related to a
function.
Variable names used in the sets of strings ~rd
and ~wr
are relative
to the function 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 into the whole
project.
~scope
removed.val select_func_lval : set ->
Slicing.Api.Mark.t ->
Datatype.String.Set.t -> Cil_types.kernel_function -> set
To select lvalues (given as a string) related to a function.
Variable names used in the sets of strings lval_str
string are
relative 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_return : set ->
spare:bool -> Cil_types.kernel_function -> set
To select the function result (returned value).
val select_func_calls_to : set ->
spare:bool -> Cil_types.kernel_function -> set
To select every calls to the given function, i.e. the call keeps its semantics in the slice.
val select_func_calls_into : set ->
spare:bool -> Cil_types.kernel_function -> set
To select every calls to the given function without the selection of its inputs/outputs.
val select_func_annots : set ->
Slicing.Api.Mark.t ->
spare:bool ->
threat:bool ->
user_assert:bool ->
slicing_pragma:bool ->
loop_inv:bool ->
loop_var:bool -> Cil_types.kernel_function -> set
To select the annotations related to a function.
val select_func_zone : set ->
Slicing.Api.Mark.t ->
Locations.Zone.t -> Cil_types.kernel_function -> set
To select an output zone related to a function.
val select_stmt_zone : set ->
Slicing.Api.Mark.t ->
Locations.Zone.t ->
before:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> set
To select a zone value related to a statement. Note: add also a transparent selection on the whole statement.
val select_stmt_term : set ->
Slicing.Api.Mark.t ->
Cil_types.term ->
Cil_types.stmt -> Cil_types.kernel_function -> set
To select a predicate value related to a statement. Note: add also a transparent selection on the whole statement.
val select_stmt_pred : set ->
Slicing.Api.Mark.t ->
Cil_types.predicate ->
Cil_types.stmt -> Cil_types.kernel_function -> set
To select a predicate value related to a statement. Note: add also a transparent selection on the whole statement.
val select_stmt_annot : set ->
Slicing.Api.Mark.t ->
spare:bool ->
Cil_types.code_annotation ->
Cil_types.stmt -> Cil_types.kernel_function -> set
To select the annotations related to a statement. Note: add also a transparent selection on the whole statement.
val select_pdg_nodes : set ->
Slicing.Api.Mark.t ->
PdgTypes.Node.t list -> Cil_types.kernel_function -> set
To select nodes of the PDG
is_ctrl_mark m
,
propagate ctrl_mark on ctrl dependenciesis_addr_mark m
,
propagate addr_mark on addr dependenciesis_data_mark m
,
propagate data_mark on data dependenciesval get_function : t -> Cil_types.kernel_function
May be used to get the function related to an internal selection.
val merge_internal : t -> t -> t
val add_to_selects_internal : t -> set -> set
val iter_selects_internal : (t -> unit) -> set -> unit
val fold_selects_internal : ('a -> t -> 'a) -> 'a -> set -> 'a
val select_stmt_internal : Cil_types.kernel_function ->
?select:t ->
Cil_types.stmt -> Slicing.Api.Mark.t -> t
May be used to select a statement :
is_ctrl_mark m
,
propagates ctrl_mark on ctrl dependencies of the statementis_addr_mark m
,
propagates addr_mark on addr dependencies of the statementis_data_mark m
,
propagates data_mark on data dependencies of the statementSlicingTypes.NoPdg
when there is no PDG for the
kernel_function
(related to PdgTypes.Pdg.is_top
).val select_label_internal : Cil_types.kernel_function ->
?select:t ->
Cil_datatype.Logic_label.t -> Slicing.Api.Mark.t -> t
May be used to select a label.
val select_min_call_internal : Cil_types.kernel_function ->
?select:t ->
Cil_types.stmt -> Slicing.Api.Mark.t -> t
May be used to select a statement call without its
inputs/outputs so that it doesn't select the statements computing the
inputs of the called function as select_stmt_internal
would do.
Invalid_argument
when the stmt
isn't a call.SlicingTypes.NoPdg
when there is no PDG for the
kernel_function
(related to PdgTypes.Pdg.is_top
).val select_stmt_zone_internal : Cil_types.kernel_function ->
?select:t ->
Cil_types.stmt ->
before:bool -> Locations.Zone.t -> Slicing.Api.Mark.t -> t
May be used to select a zone value at a program point.
SlicingTypes.NoPdg
when there is no PDG for the
kernel_function
(related to PdgTypes.Pdg.is_top
).val select_zone_at_entry_point_internal : Cil_types.kernel_function ->
?select:t ->
Locations.Zone.t -> Slicing.Api.Mark.t -> t
May be used to select a zone value at the beginning of a function.
For a defined function, it is similar to select_stmt_zone_internal
with the initial statement, but it can also be used for undefined
functions.
SlicingTypes.NoPdg
when there is no PDG for the
kernel_function
(related to PdgTypes.Pdg.is_top
).val select_zone_at_end_internal : Cil_types.kernel_function ->
?select:t ->
Locations.Zone.t -> Slicing.Api.Mark.t -> t
May be used to select a zone value at the end of a function.
For a defined function, it is similar to select_stmt_zone_internal
with the return statement, but it can also be used for undefined
functions.
SlicingTypes.NoPdg
when there is no PDG for the
kernel_function
(related to PdgTypes.Pdg.is_top
).val select_modified_output_zone_internal : Cil_types.kernel_function ->
?select:t ->
Locations.Zone.t -> Slicing.Api.Mark.t -> t
May be used to select the statements that modify the given zone considered as in output. Be careful that it is NOT the same as selecting the zone at the end! (the 'undef' zone is not propagated...).
val select_stmt_ctrl_internal : Cil_types.kernel_function ->
?select:t -> Cil_types.stmt -> t
May be used to select a statement reachability : Only propagate a ctrl_mark on the statement control dependencies.
SlicingTypes.NoPdg
when there is no PDG for the
kernel_function
(related to PdgTypes.Pdg.is_top
).val select_entry_point_internal : Cil_types.kernel_function ->
?select:t -> Slicing.Api.Mark.t -> t
val select_return_internal : Cil_types.kernel_function ->
?select:t -> Slicing.Api.Mark.t -> t
val select_decl_var_internal : Cil_types.kernel_function ->
?select:t ->
Cil_types.varinfo -> Slicing.Api.Mark.t -> t
val select_pdg_nodes_internal : Cil_types.kernel_function ->
?select:t ->
PdgTypes.Node.t list -> Slicing.Api.Mark.t -> t
May be used to select PDG nodes.
val pretty : Stdlib.Format.formatter -> t -> unit
May be used for debugging... Pretty mark information.