package frama-c

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

Module PdgIndex.FctIndexSource

Mapping between the function elements we are interested in and some * information. Used for instance to associate the nodes with the statements, * or the marks in a slice.

Sourcetype ('ni, 'ci) t

this type is used to build indexes between program objects and some information such as the PDG nodes or the slicing marks.

  • 'ni if the type of the information to store for each element,
  • 'ci if the type of the information that can be attached to call statements (calls are themselves composed of several elements, so 'ni information stored for each of them ('ni Signature.t))
Sourceval create : int -> ('ni, 'ci) t
Sourceval length : ('ni, 'ci) t -> int
Sourceval copy : ('ni, 'ci) t -> ('ni, 'ci) t

just copy the mapping

Sourceval merge : ('ni, 'ci) t -> ('ni, 'ci) t -> ('ni -> 'ni -> 'ni) -> ('ci -> 'ci -> 'ci) -> ('ni, 'ci) t

merge the two indexes using given functions merge_a and merge_b. These function are _not_ called when an element is in one index, but not the other. It is assumed that merge_x x bot = x.

Sourceval sgn : ('ni, 'ci) t -> 'ni Signature.t

get the information stored for the function signature

Sourceval find_info : ('ni, 'ci) t -> Key.t -> 'ni

find the information stored for the key. Cannot be used for Key.CallStmt keys because the type of the stored information is not the same. See find_call instead.

Sourceval find_all : ('ni, 'ci) t -> Key.t -> 'ni list

same than find_info except for call statements for which it gives the list of all the information in the signature of the call.

Sourceval find_label : ('ni, 'ci) t -> Frama_c_kernel.Cil_types.label -> 'ni

Similar to find_info for a label

Sourceval find_call : ('ni, 'ci) t -> Frama_c_kernel.Cil_types.stmt -> 'ci option * 'ni Signature.t

find the information stored for the call and its signature

Sourceval find_call_key : ('ni, 'ci) t -> Key.t -> 'ci option * 'ni Signature.t
Sourceval find_info_call : ('ni, 'ci) t -> Frama_c_kernel.Cil_types.stmt -> 'ci

find the information stored for the call

Sourceval find_info_call_key : ('ni, 'ci) t -> Key.t -> 'ci
Sourceval fold_calls : (Frama_c_kernel.Cil_types.stmt -> ('ci option * 'ni Signature.t) -> 'c -> 'c) -> ('ni, 'ci) t -> 'c -> 'c
Sourceval fold : (Key.key -> 'ni -> 'a -> 'a) -> ('ni, 'ci) t -> 'a -> 'a
Sourceval add : ('ni, 'ci) t -> Key.t -> 'ni -> unit

store the information for the key.

  • raises AddError

    if there is already something stored.

Sourceval add_or_replace : ('ni, 'ci) t -> Key.t -> 'ni -> unit

store the information for the key. Replace the previously stored information if any.

Sourceval add_info_call : ('ni, 'ci) t -> Frama_c_kernel.Cil_types.stmt -> 'ci -> replace:bool -> unit
Sourceval add_info_call_key : ('ni, 'ci) t -> Key.t -> 'ci -> replace:bool -> unit

Structural destructor for unmarshaling

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