module F_Fct: functor (
M
:
Mark
) ->
sig
.. end
If the marks provided by the user respect some constraints (see
Mark
),
we have that, after the marks propagation,
the mark of a node are always smaller than the sum of the marks of its
dependencies. It means that the mark of the statement
x = a + b;
have to be smaller that the mark of
a
plus the mark of
b
at this point.
If the marks are used for visibility for instance,
it means that if this statement is visible,
so must be the computation of a
and b
, but a
and/or b
can be
visible while x
is not.
type
mark = M.t
type
call_info = M.call_info
type
fi = (mark, call_info) PdgIndex.FctIndex.t
type
t = PdgTypes.Pdg.t * fi
type
mark_info_inter = mark PdgMarks.info_inter
val empty_to_prop : 'a list * 'b list
val create : 'a -> 'a * ('b, 'c) PdgIndex.FctIndex.t
val get_idx : 'a * 'b -> 'b
val mark_and_propagate : PdgTypes.Pdg.t * (M.t, 'a) PdgIndex.FctIndex.t ->
?to_prop:(PdgIndex.Signature.in_key * M.t) list *
(Cil_types.stmt * (PdgIndex.Signature.out_key * M.t) list) list ->
(PdgMarks.select_elem * M.t) list ->
(PdgIndex.Signature.in_key * M.t) list *
(Cil_types.stmt * (PdgIndex.Signature.out_key * M.t) list) list