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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct