module MarkPair: sig
.. end
val mk_m1_spare : SlicingInternals.pdg_mark
val mk_gen_spare : SlicingInternals.pdg_mark
val is_top : SlicingInternals.pdg_mark -> bool
val is_ctrl : SlicingInternals.pdg_mark -> bool
val is_addr : SlicingInternals.pdg_mark -> bool
val is_data : SlicingInternals.pdg_mark -> bool
val is_spare : SlicingInternals.pdg_mark -> bool
val compare : SlicingInternals.pdg_mark -> SlicingInternals.pdg_mark -> int
val _is_included : SlicingInternals.pdg_mark -> SlicingInternals.pdg_mark -> bool
val pretty : Format.formatter -> SlicingInternals.pdg_mark -> unit
val to_string : SlicingInternals.pdg_mark -> string
val minus : SlicingInternals.pdg_mark ->
SlicingInternals.pdg_mark -> SlicingInternals.pdg_mark
val merge : SlicingInternals.pdg_mark ->
SlicingInternals.pdg_mark -> SlicingInternals.pdg_mark
val merge_user_marks : SlicingInternals.pdg_mark ->
SlicingInternals.pdg_mark -> SlicingInternals.pdg_mark
merge only ma_1 et mb_1, m_2 is always bottom
val merge_all : SlicingInternals.pdg_mark list -> SlicingInternals.pdg_mark
val inter : SlicingInternals.pdg_mark ->
SlicingInternals.pdg_mark -> SlicingInternals.pdg_mark
val inter_all : SlicingInternals.pdg_mark list -> SlicingInternals.pdg_mark
val combine : SlicingInternals.pdg_mark ->
SlicingInternals.pdg_mark ->
SlicingInternals.pdg_mark * SlicingInternals.pdg_mark
combine ma mb
is used to add the mb
to the ma
.
Returns two marks : the first one is the new mark (= merge),
and the second is the one to propagate.
Notice that if the mark to propagate is bottom,
it means that mb
was included in ma
.
val missing_output : call:SlicingInternals.pdg_mark ->
called:SlicingInternals.pdg_mark -> SlicingInternals.pdg_mark option
we want to know if the called function g
with output marks
m_out_called
compute enough things to be used in f
call
with output marks m_out_call
.
Remember the mf1
marks propagates as mg2
and the marks to add
can only be m2
marks.
TODO : write this down in the specification
and check with Patrick if it is ok.
val missing_input : call:SlicingInternals.pdg_mark ->
called:SlicingInternals.pdg_mark -> SlicingInternals.pdg_mark option
tells if the caller (f
) computes enough inputs for the callee (g
).
Remember that mg1
has to be propagated as mf1
,
but mg2
has to be propagated as mf2=spare