Module Slicing.Api.Mark

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 : Stdlib.Format.formatter -> t -> unit

May be used for debugging... Pretty mark information.