Module Marks

module Marks: sig .. end

val in_marks_to_caller : PdgTypes.Pdg.t ->
       Cil_types.stmt ->
       'mark PdgMarks.m2m ->
       ?rqs:'mark PdgMarks.select ->
       'mark PdgMarks.info_caller_inputs -> 'mark PdgMarks.select

in_marks_to_caller translate the input information part returned by mark_and_propagate into (node, mark) list related to a call. Example : if marks has been propagated in f and some input marks has changed, they have to be propagated into f callers. So this function takes one call to f and translate input keys into nodes.

The function (m2m) is called for each element to translate. See m2m for more information about how to use it.

compute the marks to propagate in the caller nodes from the marks of a function inputs in_marks.

val translate_in_marks : PdgTypes.Pdg.t ->
       'mark PdgMarks.info_caller_inputs ->
       ?m2m:'mark PdgMarks.call_m2m ->
       'mark PdgMarks.pdg_select -> 'mark PdgMarks.pdg_select

translate the input information part returned by mark_and_propagate using in_marks_to_caller for each call. (see above)

some new input marks has been added in a called function. Build the list of what is to be propagated in the callers. Be careful that some Pdg can be top : in that case, a list of mark is returned (Beware that m2m has NOT been called in that case).

val call_out_marks_to_called : PdgTypes.Pdg.t ->
       'mark PdgMarks.m2m ->
       ?rqs:'mark PdgMarks.select ->
       (PdgIndex.Signature.out_key * 'mark) list -> 'mark PdgMarks.select

we have a list of a call output marks, and we want to translate it into a list of marks on the called function nodes. The pdg is the called_pdg.

val translate_marks_to_prop : PdgTypes.Pdg.t ->
       'mark PdgMarks.info_inter ->
       ?in_m2m:'mark PdgMarks.call_m2m ->
       ?out_m2m:'mark PdgMarks.call_m2m ->
       'mark PdgMarks.pdg_select -> 'mark PdgMarks.pdg_select

use both translate_in_marks and call_out_marks_to_called to translate the information provided by mark_and_propagate info selection on other functions.

add_new_marks_to_rqs pdg new_marks other_rqs translates new_marks that were computed during intraprocedural propagation into requests, and add them to other_rqs.

The functions in_m2m and out_m2m can be used to modify the marks during propagation :

in_m2m call_stmt call_in_node mark : provide the mark to propagate to the call_in_node knowing that the mark of the called function has been modify to mark
out_m2m out_node mark : provide the mark to propagate to the out_node knowing that a call output mark has been modify to mark.

module F_Proj: functor (C : PdgMarks.Config) -> Proj  with type mark = C.M.t
        and type call_info = C.M.call_info

To also use interprocedural propagation, the user can instantiate this functor.