Module Marks

module Marks: sig .. end

val in_marks_to_caller : Db.Pdg.t ->
       Cil_types.stmt ->
       (PdgMarks.select_elem -> 'a -> 'b option) ->
       ?rqs:'b PdgMarks.select ->
       (PdgIndex.Signature.in_key * 'a) list -> 'b PdgMarks.select

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

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.

val translate_in_marks : PdgTypes.Pdg.t ->
       (PdgIndex.Signature.in_key * 'a) list ->
       ?m2m:(Cil_types.stmt option ->
             Db.Pdg.t -> PdgMarks.select_elem -> 'a -> 'a option) ->
       (Db.Pdg.t * 'a PdgMarks.pdg_select_info) list ->
       (Db.Pdg.t * 'a PdgMarks.pdg_select_info) list

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).

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

val call_out_marks_to_called : PdgTypes.Pdg.t ->
       (PdgMarks.select_elem -> 'a -> 'b option) ->
       ?rqs:(PdgMarks.select_elem * 'b) list ->
       (PdgIndex.Signature.out_key * 'a) list -> (PdgMarks.select_elem * 'b) list

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_out_mark : 'a ->
       (Cil_types.stmt option -> Db.Pdg.t -> PdgMarks.select_elem -> 'b -> 'c option) ->
       (Db.Pdg.t * 'c PdgMarks.pdg_select_info) list ->
       Cil_types.stmt * (PdgIndex.Signature.out_key * 'b) list ->
       (Db.Pdg.t * 'c PdgMarks.pdg_select_info) list

val translate_marks_to_prop : PdgTypes.Pdg.t ->
       (PdgIndex.Signature.in_key * 'a) list *
       (Cil_types.stmt * (PdgIndex.Signature.out_key * 'a) list) list ->
       ?in_m2m:(Cil_types.stmt option ->
                Db.Pdg.t -> PdgMarks.select_elem -> 'a -> 'a option) ->
       ?out_m2m:(Cil_types.stmt option ->
                 Db.Pdg.t -> PdgMarks.select_elem -> 'a -> 'a option) ->
       (Db.Pdg.t * 'a PdgMarks.pdg_select_info) list ->
       (Db.Pdg.t * 'a PdgMarks.pdg_select_info) list

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.

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.

module F_Proj: 
functor (C : PdgMarks.Config) -> sig .. end

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