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 ->
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 whole scope of the function.
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.
Change in Magnesium-20151001: argument ~scope
removed.
val select_stmt_lval : (set ->
Db.Slicing.Mark.t ->
Datatype.String.Set.t ->
before:bool ->
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 whole scope of the function.
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.
Change in Magnesium-20151001: argument ~scope
removed.
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.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 ->
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 whole scope of the function.
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.
Change in Magnesium-20151001: argument ~scope
removed.
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 functional 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 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)
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