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
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
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