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:
To also use interprocedural propagation, the user can instantiate this functor.