Frama-C:
Plug-ins:
Libraries:

Frama-C API - Mark

Access to slicing results.

Abstract data type for mark value.

For dynamic type checking.

No needs of 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. That mark is related to transparent selection.

val is_ctrl : t -> bool

The element is used to control the program point of a selected data.

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_addr : t -> bool

The element is used to compute the address of a selected data.

val get_from_src_func : Frama_c_kernel.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)

Debug

val pretty : Stdlib.Format.formatter -> t -> unit