module Spare_marks:sig
..end
FctIndex
marked with BoolMark
to be used by Pdg.Register.F_Proj
, and another table to store if a function
is visible (usefull for Top PDG).
Useful mainly if there has been some Pdg.Top
val debug : int -> ('a, Format.formatter, unit) Pervasives.format -> 'a
val fatal : ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
FctIndex
marked with BoolMark
to be used by Pdg.Register.F_Proj
, and another table to store if a function
is visible (usefull for Top PDG).module BoolMark:sig
..end
module KfTopVisi:sig
..end
val call_in_to_check : (Db.Pdg.t * Cil_types.stmt option * PdgMarks.select_elem *
(bool * BoolMark.prop_mode))
list Pervasives.ref
val called_top : Kernel_function.Hptset.elt list Pervasives.ref
module Config:sig
..end
module ProjBoolMarks:Pdg.Register.F_Proj
(
Config
)
typeproj =
ProjBoolMarks.t * unit KfTopVisi.t
typefct =
ProjBoolMarks.fct
val new_project : unit -> ProjBoolMarks.t * 'a KfTopVisi.t
val proj_marks : 'a * 'b -> 'a
val get_marks : ProjBoolMarks.t * 'a KfTopVisi.t ->
KfTopVisi.key -> ProjBoolMarks.fct option
Not_found
when the function is not marked. It might be the case
that it is nonetheless visible, but has no marks because of a Top PDG.val kf_visible : ProjBoolMarks.t * 'a KfTopVisi.t ->
KfTopVisi.key -> bool
Useful mainly if there has been some Pdg.Top
val key_visible : (bool * 'a, 'b) PdgIndex.FctIndex.t -> PdgIndex.Key.t -> bool
val call_visible : (bool * 'a, 'b) PdgIndex.FctIndex.t -> Cil_types.stmt -> bool
val add_pdg_selection : (Db.Pdg.t * 'a list) list ->
Db.Pdg.t -> 'a option -> (Db.Pdg.t * 'a list) list
val add_node_to_select : bool ->
(bool * BoolMark.prop_mode) PdgMarks.select ->
Locations.Zone.t option ->
PdgTypes.Node.t -> (bool * BoolMark.prop_mode) PdgMarks.select
val add_nodes_and_undef_to_select : bool ->
PdgTypes.Node.t list * PdgTypes.Node.t list *
((PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option)
option ->
(bool * BoolMark.prop_mode) PdgMarks.select ->
(bool * BoolMark.prop_mode) PdgMarks.select
val select_pdg_elements : ProjBoolMarks.t * unit KfTopVisi.t ->
PdgTypes.Pdg.t -> ProjBoolMarks.mark PdgMarks.select -> unit
val process_call_inputs : ProjBoolMarks.t * unit KfTopVisi.t -> unit
proj
contains some function marks and !call_in_to_check
is a list of call input marks to propagate when the call is visible.
These marks come from the called function selection,
but they are not automatically propagated because when a function is visible
it doesn't mean that all the calls to that function are visible.
So we first split the todo list (!call_in_to_check
) into the nodes to mark
which correspond to inputs of visible calls
and the others that do not yet correspond to visible call
but we keep them because it can happen later
val select_entry_point : ProjBoolMarks.t * unit KfTopVisi.t ->
'a -> Db.Pdg.t -> unit
val select_all_outputs : ProjBoolMarks.t * unit KfTopVisi.t ->
Cil_types.kernel_function -> Db.Pdg.t -> unit
class annot_visitor :filter:(Cil_types.code_annotation -> bool) -> Db.Pdg.t ->
object
..end
val select_annotations : select_annot:bool ->
select_slice_pragma:bool ->
ProjBoolMarks.t * unit KfTopVisi.t -> unit
val finalize : ProjBoolMarks.t * unit KfTopVisi.t -> unit
val select_useful_things : select_annot:bool ->
select_slice_pragma:bool ->
Kernel_function.t ->
ProjBoolMarks.t * unit KfTopVisi.t