package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Api.MarkSource

Access to slicing results.

Abstract data type for mark value.

For dynamic type checking.

No needs of Journalization

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

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

Sourceval is_bottom : t -> bool

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

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

Sourceval is_ctrl : t -> bool

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

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

Sourceval is_addr : t -> bool

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)

Debug

Sourceval pretty : Format.formatter -> t -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct