Frama-C:
Plug-ins:
Libraries:

Frama-C API - Builtin_functions

A list of the built-in functions for the current compiler (GCC or MSVC, depending on !Machine.msvcMode). Maps the name to the result and argument types, and whether it is vararg. Initialized by Machine.init. Do not add builtins directly, use add_custom_builtin below for that.

This map replaces gccBuiltins and msvcBuiltins in previous versions of CIL.

Hashtbl are a standard computation. BUT that is INCORRECT to use projectified hashtables if keys have a custom rehash function (see Datatype.Make_input.rehash)

include State_builder.S
val self : State.t

The kind of the registered state.

val name : string
val mark_as_computed : ?project:Project.t -> unit -> unit

Indicate that the registered state will not change again for the given project (default is current ()).

val is_computed : ?project:Project.t -> unit -> bool

Returns true iff the registered state will not change again for the given project (default is current ()).

Exportation of some inputs (easier use of State_builder.Register).

val add_hook_on_update : (Datatype.t -> unit) -> unit

Add an hook which is applied each time (just before) the project library changes the local value of the state.

  • since Nitrogen-20111001
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit

howto_marshal marshal unmarshal registers a custom couple of functions (marshal, unmarshal) to be used for serialization. Default functions are identities. In particular, this function must be used if Datatype.t is not marshallable and do_not_save is not called.

  • since Boron-20100401
type key = string
type data = Cil_types.typ * Cil_types.typ list * bool
val replace : key -> data -> unit

Add a new binding. The previous one is removed.

val add : key -> data -> unit

Add a new binding. The previous one is only hidden.

val clear : unit -> unit

Clear the table.

val length : unit -> int

Length of the table.

val iter : (key -> data -> unit) -> unit
val iter_sorted : ?cmp:(key -> key -> int) -> (key -> data -> unit) -> unit
val fold : (key -> data -> 'a -> 'a) -> 'a -> 'a
val fold_sorted : ?cmp:(key -> key -> int) -> (key -> data -> 'a -> 'a) -> 'a -> 'a
val memo : ?change:(data -> data) -> (key -> data) -> key -> data

Memoization. Compute on need the data associated to a given key using the given function. If the data is already computed, it is possible to change with change.

val find : key -> data

Return the current binding of the given key.

  • raises Not_found

    if the key is not in the table.

val find_opt : key -> data option

Return the current binding of the given key, or None if no such binding exists.

  • since 27.0-Cobalt
val find_all : key -> data list

Return the list of all data associated with the given key.

val mem : key -> bool
val remove : key -> unit
val to_seq : unit -> (key * data) Stdlib.Seq.t

Iterate on the whole table.

  • since 27.0-Cobalt
val add_hook_on_change : ((key, data) State_builder.hashtbl_event -> unit) -> unit

Add an hook which is applied each time (just after) a (key,value) pair in the hashtable changes inside the current project.

  • since 28.0-Nickel