package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 PdgMarks.m2m for more information about how to use it.

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

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.

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.