Module SlicingMarks.MarkPair

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
see SlicingMarks.Mark.merge
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