package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
module M : Mark
val mark_to_prop_to_caller_input : M.t call_m2m

define how to translate an input mark of a function into a mark * to propagate in the callers. * The statement specify to which call we are about to propagate, * and the pdg is the one of the caller in which the call is. * If it returns None, the propagation is stopped. * A simple propagation can be done by returning Some m. * The call parameter can be None when the caller has a Top PDG. *

val mark_to_prop_to_called_output : M.t call_m2m

define how to translate a mark of a call output into a mark * to propagate in the called function. * The statement specify from which call we are about to propagate, * and the pdg is the one of the called function. *