package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-pdg.core/Pdg/Marks/F_Proj/argument-1-C/index.html

Parameter `F_Proj.C`

module M : Pdg_types.PdgMarks.Mark

val mark_to_prop_to_caller_input : M.t Pdg_types.PdgMarks.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 Pdg_types.PdgMarks.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.