Module Pdg_types.PdgMarks

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

module type Mark = sig ... end

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

type select_elem = private
| SelNode of PdgTypes.Node.t * Frama_c_kernel.Locations.Zone.t option
| 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. *

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

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

type 'tm pdg_select = (PdgTypes.Pdg.t * 'tm pdg_select_info) list
type '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. *

type '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.

type '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.

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

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

module type Config = sig ... end