module Select: sig
.. end
Slicing selections.
type
t = SlicingTypes.sl_select
Internal selection.
val dyn_t : t Type.t
For dynamic type checking and journalization.
type
set = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t
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)
Pervasives.ref
To select a statement.
val select_stmt_ctrl : (set ->
spare:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> set)
Pervasives.ref
To select a statement reachability.
Note: add also a transparent selection on the whole statement.
val select_stmt_lval_rw : (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 -> Cil_types.kernel_function -> set)
Pervasives.ref
To select rw accesses to lvalues (given as string) related 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 contained into the statement ki
.
Note: add also a transparent selection on the whole statement.
val select_stmt_lval : (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 -> set)
Pervasives.ref
To select lvalues (given as string) related 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 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.
val select_stmt_zone : (set ->
Db.Slicing.Mark.t ->
Locations.Zone.t ->
before:bool ->
Cil_types.stmt -> Cil_types.kernel_function -> set)
Pervasives.ref
To select a zone value related to a statement.
Note: add also a transparent selection on the whole statement.
val select_stmt_term : (set ->
Db.Slicing.Mark.t ->
Cil_types.term ->
Cil_types.stmt -> Cil_types.kernel_function -> set)
Pervasives.ref
To select a predicate value related to a statement.
Note: add also a transparent selection on the whole statement.
val select_stmt_pred : (set ->
Db.Slicing.Mark.t ->
Cil_types.predicate Cil_types.named ->
Cil_types.stmt -> Cil_types.kernel_function -> set)
Pervasives.ref
To select a predicate value related to a statement.
Note: add also a transparent selection on the whole statement.
val select_stmt_annot : (set ->
Db.Slicing.Mark.t ->
spare:bool ->
Cil_types.code_annotation ->
Cil_types.stmt -> Cil_types.kernel_function -> set)
Pervasives.ref
To select the annotations related to a statement.
Note: add also a transparent selection on the whole statement.
val select_stmt_annots : (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 -> set)
Pervasives.ref
To select the annotations related to a statement.
Note: add also a transparent selection on the whole statement.
val select_func_lval_rw : (set ->
Db.Slicing.Mark.t ->
rd:Datatype.String.Set.t ->
wr:Datatype.String.Set.t ->
scope:Cil_types.stmt ->
eval:Cil_types.stmt -> Cil_types.kernel_function -> set)
Pervasives.ref
To select rw accesses to lvalues (given as a string) related to a function.
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 value of these lvalues into the whole project.
val select_func_lval : (set ->
Db.Slicing.Mark.t ->
Datatype.String.Set.t -> Cil_types.kernel_function -> set)
Pervasives.ref
To select lvalues (given as a string) related to a function.
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_zone : (set ->
Db.Slicing.Mark.t ->
Locations.Zone.t -> Cil_types.kernel_function -> set)
Pervasives.ref
To select an output zone related to a function.
val select_func_return : (set ->
spare:bool -> Cil_types.kernel_function -> set)
Pervasives.ref
To select the function result (returned value).
val select_func_calls_to : (set ->
spare:bool -> Cil_types.kernel_function -> set)
Pervasives.ref
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)
Pervasives.ref
To select every calls to the given function without the selection of
its inputs/outputs.
val select_func_annots : (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 -> set)
Pervasives.ref
To select the annotations related to a function.
Internal use only
val pretty : (Format.formatter -> t -> unit) Pervasives.ref
For debugging... Pretty print selection information.
val get_function : (t -> Cil_types.kernel_function) Pervasives.ref
The function related to an internal selection.
val merge_internal : (t -> t -> t)
Pervasives.ref
The function related to an internal selection.
val add_to_selects_internal : (t -> set -> set)
Pervasives.ref
val iter_selects_internal : ((t -> unit) -> set -> unit)
Pervasives.ref
val fold_selects_internal : ('a -> t -> 'a) -> 'a -> set -> 'a
val select_stmt_internal : (Cil_types.kernel_function ->
?select:t ->
Cil_types.stmt -> Db.Slicing.Mark.t -> t)
Pervasives.ref
Internally used to select a statement :
- if
is_ctrl_mark m
,
propagate ctrl_mark on ctrl dependencies of the statement
- if
is_addr_mark m
,
propagate addr_mark on addr dependencies of the statement
- if
is_data_mark m
,
propagate data_mark on data dependencies of the statement
- mark the node with a spare_mark and propagate so that
the dependencies that were not selected yet will be marked spare.
When the statement is a call, its functionnal inputs/outputs are
also selected (The call is still selected even it has no output).
When the statement is a composed one (block, if, etc...),
all the sub-statements are selected.
Raises SlicingTypes.NoPdg
if ?
val select_label_internal : (Cil_types.kernel_function ->
?select:t ->
Cil_datatype.Logic_label.t -> Db.Slicing.Mark.t -> t)
Pervasives.ref
val select_min_call_internal : (Cil_types.kernel_function ->
?select:t ->
Cil_types.stmt -> Db.Slicing.Mark.t -> t)
Pervasives.ref
Internally 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.
Raise Invalid_argument
when the stmt
isn't a call.
Raises SlicingTypes.NoPdg
if ?
val select_stmt_zone_internal : (Cil_types.kernel_function ->
?select:t ->
Cil_types.stmt ->
before:bool -> Locations.Zone.t -> Db.Slicing.Mark.t -> t)
Pervasives.ref
Internally used to select a zone value at a program point.
Raises SlicingTypes.NoPdg
if ?
val select_zone_at_entry_point_internal : (Cil_types.kernel_function ->
?select:t ->
Locations.Zone.t -> Db.Slicing.Mark.t -> t)
Pervasives.ref
Internally 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.
Raises SlicingTypes.NoPdg
if ?
val select_zone_at_end_internal : (Cil_types.kernel_function ->
?select:t ->
Locations.Zone.t -> Db.Slicing.Mark.t -> t)
Pervasives.ref
Internally 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.
Raises SlicingTypes.NoPdg
if ?
val select_modified_output_zone_internal : (Cil_types.kernel_function ->
?select:t ->
Locations.Zone.t -> Db.Slicing.Mark.t -> t)
Pervasives.ref
Internally used to select the statements that modify the
given zone considered as in output.
Be careful that it is NOT the same than selectiong the zone at end !
( the 'undef' zone is not propagated...)
val select_stmt_ctrl_internal : (Cil_types.kernel_function ->
?select:t -> Cil_types.stmt -> t)
Pervasives.ref
Internally used to select a statement reachability :
Only propagate a ctrl_mark on the statement control dependencies.
Raises SlicingTypes.NoPdg
if ?
val select_pdg_nodes_internal : (Cil_types.kernel_function ->
?select:t ->
PdgTypes.Node.t list -> Db.Slicing.Mark.t -> t)
Pervasives.ref
Internally used to select PDG nodes :
- if
is_ctrl_mark m
,
propagate ctrl_mark on ctrl dependencies of the statement
- if
is_addr_mark m
,
propagate addr_mark on addr dependencies of the statement
- if
is_data_mark m
,
propagate data_mark on data dependencies of the statement
- mark the node with a spare_mark and propagate so that
the dependencies that were not selected yet will be marked spare.
val select_entry_point_internal : (Cil_types.kernel_function ->
?select:t -> Db.Slicing.Mark.t -> t)
Pervasives.ref
val select_return_internal : (Cil_types.kernel_function ->
?select:t -> Db.Slicing.Mark.t -> t)
Pervasives.ref
val select_decl_var_internal : (Cil_types.kernel_function ->
?select:t ->
Cil_types.varinfo -> Db.Slicing.Mark.t -> t)
Pervasives.ref
val select_pdg_nodes : (set ->
Db.Slicing.Mark.t ->
PdgTypes.Node.t list -> Cil_types.kernel_function -> set)
Pervasives.ref