module Db:sig
..end
Dynamic
: API for plug-ins linked dynamicallyJournal
: journalisationLog
: message outputs and printersPlugin
: general services for plug-insProject
and associated files: Kind
, Datatype
and State_builder
.Ast
: the cil ASTAst_info
: syntactic value directly computed from the Cil AstFile
: Cil file initializationGlobals
: global variables, functions and annotationsAnnotations
: annotations associated with a statementProperties_status
: status of annotationsKernel_function
: C functions as seen by Frama-CStmts_graph
: the statement graphLoop
: (natural) loopsVisitor
: frama-c visitorsKernel
: general parameters of Frama-C (mostly set from the command
line)type 'a
how_to_journalize =
| |
Journalize of |
(* |
Journalize the value with the given name and type.
| *) |
| |
Journalization_not_required |
(* |
Journalization of this value is not required
(usually because it has no effect on the Frama-C global state).
| *) |
| |
Journalization_must_not_happen of |
(* |
Journalization of this value should not happen
(usually because it is a low-level function: this function is always
called from a journalized function).
The string is the function name which is used for displaying suitable
error message.
| *) |
val register : 'a how_to_journalize -> 'a Pervasives.ref -> 'a -> unit
val register_compute : string ->
State.t list -> (unit -> unit) Pervasives.ref -> (unit -> unit) -> State.t
val register_guarded_compute : string ->
(unit -> bool) -> (unit -> unit) Pervasives.ref -> (unit -> unit) -> unit
module Main:sig
..end
module Toplevel:sig
..end
module Value:sig
..end
module From:sig
..end
module Properties:sig
..end
module PostdominatorsTypes:sig
..end
module Postdominators:PostdominatorsTypes.Sig
module PostdominatorsValue:PostdominatorsTypes.Sig
module RteGen:sig
..end
module Security:sig
..end
module Pdg:sig
..end
module type INOUTKF =sig
..end
module type INOUT =sig
..end
module Inputs:sig
..end
module Outputs:sig
..end
module Operational_inputs:sig
..end
val progress : (unit -> unit) Pervasives.ref
type
daemon
val on_progress : ?debounced:int -> ?on_delayed:(int -> unit) -> (unit -> unit) -> daemon
on_progress ?debounced ?on_delayed trigger
registers trigger
as new
daemon to be executed on each Db.yield
.debounced
: the least amount of time between two successive calls to the
daemon, in milliseconds (default is 0ms).on_delayed
: the callback invoked as soon as the time since the last
Db.yield
is greater than debounced
milliseconds (or 100ms at least).val off_progress : daemon -> unit
daemon
.val flush : unit -> unit
val yield : unit -> unit
val cancel : unit -> unit
val with_progress : ?debounced:int ->
?on_delayed:(int -> unit) -> (unit -> unit) -> ('a -> 'b) -> 'a -> 'b
with_progress ?debounced ?on_delayed trigger job data
executes the given
job
on data
while registering trigger
as temporary (debounced) daemon.
The daemon is finally unregistered at the end of the computation.
Illustrative example, where ...
is the debounced time:
job data : |<-------------------------------------------------->|<daemon removed>
yields : x x x x x x x x xxx xxx
trigger : |.......... |.......... |.......... |.........
delayed : !
notes : (1) (2) (3)
job
on data
.debounced
: the least amount of time, in milliseconds, between two
successive calls to the daemon (default is 0ms).on_delayed
: the callback invoked as soon as the time since the last
yield
is greater than debounced
milliseconds (or 100ms at least).val sleep : int -> unit
exception Cancel
Db.yield
to interrupt computations.