Module Marks

module Marks: sig .. end
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 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 :

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.