package frama-c

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

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.

type ('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))
val create : int -> ('ni, 'ci) t
val length : ('ni, 'ci) t -> int
val copy : ('ni, 'ci) t -> ('ni, 'ci) t

just copy the mapping

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

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

get the information stored for the function signature

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

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

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

Similar to find_info for a label

val 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

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

find the information stored for the call

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

store the information for the key.

  • raises AddError

    if there is already something stored.

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

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

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

Structural destructor for unmarshaling