Abstract data type for mark value.

For dynamic type checking.

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).

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.

true iff the mark is empty: it is the only case where the associated element is invisible.

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.

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

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.

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

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)