module Mark: sig
.. end
Access to slicing results.
type
t
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
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
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
true
iff the mark is empty: it is the only case where the
associated element is invisible.
val is_spare : t -> bool
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
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
The element is used to control the program point of a selected
data.
val is_addr : t -> bool
The element is used to compute the address of a selected data.
val get_from_src_func : Cil_types.kernel_function -> t
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)
Not for casual users
val pretty : Format.formatter -> t -> unit
May be used for debugging... Pretty mark information.