Module Spare_marks

module Spare_marks: sig .. end
The project is composed of 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

The project is composed of 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
when we first compute marks to select outputs, we don't immediately propagate input marks to the calls, because some calls may be useless and we don't want to compute their inputs. We will check calls later on. But when we select annotations, we want to preserve all the calls that can lead to them : so, we propagate...
val called_top : Kernel_function.Hptset.elt list Pervasives.ref
module Config: sig .. end
module ProjBoolMarks: Pdg.Register.F_Proj(Config)
type proj = ProjBoolMarks.t * unit KfTopVisi.t 
type fct = ProjBoolMarks.fct 
val new_project : unit -> ProjBoolMarks.t * 'a KfTopVisi.t

Get stored information
val proj_marks : 'a * 'b -> 'a
val get_marks : ProjBoolMarks.t * 'a KfTopVisi.t ->
KfTopVisi.key -> ProjBoolMarks.fct option
Raises 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 only if there has been some Pdg.Top

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
the call is visible if its control node is visible

Build selections and propagate.
val add_pdg_selection : (Db.Pdg.t * 'a list) list ->
Db.Pdg.t -> 'a option -> (Db.Pdg.t * 'a list) list
Doesn't mark yet, but add what has to be marked in the selection, and keep things sorted.
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
Mark the function as visible and add the marks according to the selection. Notice that if the function has been marked as called by a visible top, we can skip the selection since the function has to be fully visible anyway.

First step is finished: propagate in the calls.
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


Main selection: select starting points and propagate.
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
used to visit all the annotations of a given function and to find the PDG nodes to select so that the reachable annotations can be visible
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