Module Marks

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


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.