Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make_ordered

  • since Neon-20140301

Parameters

module P : sig ... end

Signature

include S with type param = unit with type result = unit
type param = unit

Type of the parameter of the functions registered in the hook.

type result = unit

Type of the result of the functions. result can be unit (for iterative hooks) or param (for folding hooks)

val apply : param -> result

Apply all the functions of the hook on the given parameter. These functions are applied from the least recently entered to the most recently entered.

val is_empty : unit -> bool

Is no function already registered in the hook?

val clear : unit -> unit

Clear the hook.

val length : unit -> int

Number of registered functions.

type key = P.Id.t
type id
val register_key : key -> id
val extend : id -> (param -> result) -> unit
val extend_once : id -> (param -> result) -> unit
val add_dependency : id -> id -> unit

add_dependency hook1 hook2 indicates that hook1 must be executed before hook2. In case of a cycle, all hooks will be executed, but an arbitrary order will be chosen among the elements of the cycle.