Frama-C API - Marks
val in_marks_to_caller : Pdg_types.PdgTypes.Pdg.t -> Frama_c_kernel.Cil_types.stmt -> 'mark Pdg_types.PdgMarks.m2m -> ?rqs:'mark Pdg_types.PdgMarks.select -> 'mark Pdg_types.PdgMarks.info_caller_inputs -> 'mark Pdg_types.PdgMarks.selectin_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 PdgMarks.m2m for more information about how to use it.
val translate_in_marks : Pdg_types.PdgTypes.Pdg.t -> 'mark Pdg_types.PdgMarks.info_caller_inputs -> ?m2m:'mark Pdg_types.PdgMarks.call_m2m -> 'mark Pdg_types.PdgMarks.pdg_select -> 'mark Pdg_types.PdgMarks.pdg_selecttranslate 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 : Pdg_types.PdgTypes.Pdg.t -> 'mark Pdg_types.PdgMarks.m2m -> ?rqs:'mark Pdg_types.PdgMarks.select -> (Pdg_types.PdgIndex.Signature.out_key * 'mark) list -> 'mark Pdg_types.PdgMarks.selectwe 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 : Pdg_types.PdgTypes.Pdg.t -> 'mark Pdg_types.PdgMarks.info_inter -> ?in_m2m:'mark Pdg_types.PdgMarks.call_m2m -> ?out_m2m:'mark Pdg_types.PdgMarks.call_m2m -> 'mark Pdg_types.PdgMarks.pdg_select -> 'mark Pdg_types.PdgMarks.pdg_selectuse 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 (C : Pdg_types.PdgMarks.Config) : Pdg_types.PdgMarks.Proj with type mark = C.M.t and type call_info = C.M.call_info