Module PdgMarks

module PdgMarks: sig .. end
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 pluggin itself (in pdg/marks): the signatures of these public functions can be found in file Pdg.mli

This file provides useful things to help to associate an information (called mark) to PDG elements and to propagate it across the dependencies.


module type Mark = sig .. end
Signature of the module to use in order to instanciate the computation
type select_elem = private 
| SelNode of PdgTypes.Node.t * Locations.Zone.t option (*
zone is Some z only for nodes that represent call output in case we want to select less than the whole OutCall
*)
| SelIn of 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:Locations.Zone.t option -> PdgTypes.Node.t -> select_elem
val mk_select_undef_zone : 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 * Locations.Zone.t option -> 'tm -> 'tm select
val add_undef_in_to_select : 'tm select -> 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 = (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: 
functor (M : Mark) -> Fct with type mark = M.t and type call_info = M.call_info
If the marks provided by the user respect some constraints (see Mark), we have that, after the marks propagation, the mark of a node are always smaller than the sum of the marks of its dependencies.
type 't_mark m2m = select_elem -> 't_mark -> 't_mark option 
type 't_mark call_m2m = 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.
module type Config = sig .. end