module FctMarks: sig
.. end
FctMarks
manages the mapping between a function elements and their
marks. See PdgIndex.FctIndex
to know what an element is.
type
t = PropMark.t
type
to_prop = PropMark.mark_info_inter
val empty_to_prop : PropMark.mark_info_inter
val new_copied_slice : SlicingInternals.fct_slice -> SlicingInternals.fct_slice
val new_init_slice : SlicingInternals.fct_info ->
PdgTypes.Pdg.t *
(PropMark.mark, PropMark.call_info)
PdgIndex.FctIndex.t -> SlicingInternals.fct_slice
Raises SlicingTypes.NoPdg
(see new_slice
)
val new_empty_slice : SlicingInternals.fct_info -> SlicingInternals.fct_slice
Raises SlicingTypes.NoPdg
(see new_slice
)
val new_empty_fi_marks : SlicingInternals.fct_info -> PropMark.t
val fi_marks : SlicingInternals.fct_info -> SlicingInternals.ff_marks option
val get_ff_marks : SlicingInternals.fct_slice -> SlicingInternals.ff_marks
val merge : SlicingInternals.fct_slice ->
SlicingInternals.fct_slice ->
PdgTypes.Pdg.t *
(SlicingTypes.sl_mark, SlicingInternals.call_info) PdgIndex.FctIndex.t
val get_node_mark : SlicingInternals.fct_slice ->
PdgIndex.Key.t -> PropMark.mark
val get_fi_node_mark : SlicingInternals.fct_info -> PdgIndex.Key.t -> SlicingTypes.sl_mark
val get_node_marks : SlicingInternals.fct_slice ->
PdgIndex.Key.t -> PropMark.mark list
val get_sgn : SlicingInternals.fct_slice ->
PropMark.mark PdgIndex.Signature.t option
val get_all_input_marks : t ->
(PdgIndex.Signature.in_key * SlicingTypes.sl_mark) list * 'a list
val get_matching_input_marks : t ->
Locations.Zone.t ->
(PdgIndex.Signature.in_key * SlicingTypes.sl_mark) list * 'a list
val fold_calls : (Cil_types.stmt -> Fct_slice.CallInfo.t -> 'a -> 'a) ->
SlicingInternals.fct_slice -> 'a -> 'a
val change_call : SlicingInternals.project ->
SlicingInternals.fct_slice ->
Cil_types.stmt -> SlicingInternals.called_fct option -> unit
val mark_and_propagate : t ->
?to_prop:PropMark.mark_info_inter ->
PropMark.mark PdgMarks.select ->
PropMark.mark_info_inter
mark the node with the given mark and propagate it to its dependencies
val marks_for_caller_inputs : PdgTypes.Pdg.t ->
t ->
Cil_types.stmt ->
SlicingTypes.sl_mark PdgMarks.info_caller_inputs * 'a ->
SlicingInternals.fct_info -> SlicingTypes.sl_mark PdgMarks.select * bool
compute the marks to propagate in pdg_caller
when the called function
have the to_prop
marks.
fi_to_call
: is used to compute more_inputs
only :
a persistent input mark is not considered as a new input.
val marks_for_call_outputs : 'a * 'b -> 'b
val get_call_output_marks : ?spare_info:(SlicingInternals.fct_slice * Cil_types.stmt) option ->
Fct_slice.CallInfo.t ->
(PdgIndex.Signature.out_key * SlicingTypes.sl_mark) list
val check_called_marks : (PdgIndex.Signature.out_key * SlicingTypes.sl_mark) list ->
SlicingInternals.fct_slice -> SlicingTypes.sl_mark PdgMarks.select * bool
val persistant_in_marks_to_prop : SlicingInternals.fct_info ->
SlicingTypes.sl_mark PdgMarks.info_caller_inputs * 'a ->
SlicingTypes.sl_mark PdgMarks.pdg_select
val get_new_marks : SlicingInternals.fct_slice ->
(PdgMarks.select_elem * SlicingTypes.sl_mark) list ->
(PdgMarks.select_elem * SlicingTypes.sl_mark) list
val mark_spare_call_nodes : SlicingInternals.fct_slice ->
Cil_types.stmt -> PropMark.mark_info_inter
val mark_visible_inputs : 'a -> 'b -> 'b
TODO :
this function should disappear when the parameter declarations will
be handled...
See TODO in Pdg.Build.do_param
val mark_visible_output : t -> unit
val debug_marked_ff : Format.formatter -> SlicingInternals.fct_slice -> unit