Module Db.Slicing.Mark

module Mark: sig .. end
Access to slicing results.

type t = SlicingTypes.sl_mark 
Abstract data type for mark value.
val dyn_t : t Type.t
For dynamic type checking and journalization.
val make : (data:bool -> addr:bool -> ctrl:bool -> t) Pervasives.ref
To construct a mark such as (is_ctrl result, is_data result, isaddr result) =
          (~ctrl, ~data, ~addr)
, (is_bottom result) = false and (is_spare result) = not (~ctrl || ~data || ~addr).
val compare : (t -> t -> int) Pervasives.ref
A total ordering function similar to the generic structural comparison function compare. Can be used to build a map from t marks to, for example, colors for the GUI.
val is_bottom : (t -> bool) Pervasives.ref
true iff the mark is empty: it is the only case where the associated element is invisible.
val is_spare : (t -> bool) Pervasives.ref
Smallest visible mark. Usually used to mark element that need to be visible for compilation purpose, not really for the selected computations.
val is_data : (t -> bool) Pervasives.ref
The element is used to compute selected data. Notice that a mark can be is_data and/or is_ctrl and/or is_addr at the same time.
val is_ctrl : (t -> bool) Pervasives.ref
The element is used to control the program point of a selected data.
val is_addr : (t -> bool) Pervasives.ref
The element is used to compute the address of a selected data.
val get_from_src_func : (Cil_types.kernel_function -> t) Pervasives.ref
The mark m related to all statements of a source function kf. Property : is_bottom (get_from_func proj kf) = not (Project.is_called proj kf) 
val pretty : (Format.formatter -> t -> unit) Pervasives.ref
For debugging... Pretty mark information.