package frama-c

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

Module Pdg_types.PdgMarksSource

This module provides elements to mapped information (here called 'marks') * to PDG elements and propagate it along the dependencies. * * Some more functions are defined in the PDG plugin itself * (in pdg/marks): * the signatures of these public functions can be found in file Pdg.mli

Sourcemodule type Mark = sig ... end

Signature of the module to use in order to instantiate the computation

Sourcetype select_elem = private
  1. | SelNode of PdgTypes.Node.t * Frama_c_kernel.Locations.Zone.t option
  2. | SelIn of Frama_c_kernel.Locations.Zone.t

When selecting or propagating marks in a function, * the marks are most of the time associated to pdg nodes, * but we also need to associate marks to input locations * in order to propage information to the callers about undefined data. *

Sourceval mk_select_node : ?z_opt:Frama_c_kernel.Locations.Zone.t option -> PdgTypes.Node.t -> select_elem
Sourcetype 'tm select = (select_elem * 'tm) list
Sourceval add_to_select : 'tm select -> select_elem -> 'tm -> 'tm select
Sourceval add_node_to_select : 'tm select -> (PdgTypes.Node.t * Frama_c_kernel.Locations.Zone.t option) -> 'tm -> 'tm select
Sourceval add_undef_in_to_select : 'tm select -> Frama_c_kernel.Locations.Zone.t option -> 'tm -> 'tm select
Sourcetype 'tm pdg_select_info =
  1. | SelList of 'tm select
  2. | SelTopMarks of 'tm list

we sometime need a list of t_select associated with its pdg when dealing with several functions at one time.

Sourcetype 'tm pdg_select = (PdgTypes.Pdg.t * 'tm pdg_select_info) list
Sourcetype 'tm info_caller_inputs = (PdgIndex.Signature.in_key * 'tm) list

Represent the information to propagate from a function inputs to its calls. Notice that the input keys don't necessarily correspond to nodes especially when one want to select a data that is not defined in the function. *

Sourcetype 'tm info_called_outputs = (Frama_c_kernel.Cil_types.stmt * (PdgIndex.Signature.out_key * 'tm) list) list

Represent the information to propagate from a call outputs to the called function. The stmt are the calls to consider.

Sourcetype 'tm info_inter = 'tm info_caller_inputs * 'tm info_called_outputs

when some marks have been propagated in a function, there is some information to propagate in the callers and called functions to have an interprocedural processing.

Sourcemodule type Fct = sig ... end
Sourcemodule F_Fct (M : Mark) : Fct with type mark = M.t and type call_info = M.call_info
Sourcetype 't_mark m2m = select_elem -> 't_mark -> 't_mark option
Sourcetype 't_mark call_m2m = Frama_c_kernel.Cil_types.stmt option -> PdgTypes.Pdg.t -> 't_mark m2m
Sourcemodule type Proj = sig ... end

this is the type of the functor dedicated to interprocedural propagation. It is defined in PDG plugin

Sourcemodule type Config = sig ... end
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