Frama_c_kernel.Db
Database in which static plugins are registered.
Modules providing general services:
Dynamic
: API for plug-ins linked dynamicallyLog
: message outputs and printersPlugin
: general services for plug-insProject
and associated files: Datatype
and State_builder
.Other main kernel modules:
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 statementProperty_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)val register_guarded_compute :
(unit -> bool) ->
(unit -> unit) Stdlib.ref ->
(unit -> unit) ->
unit
module Main : sig ... end
Frama-C main interface.
module Toplevel : sig ... end
module PostdominatorsTypes : sig ... end
Declarations common to the various postdominators-computing modules
module Postdominators : PostdominatorsTypes.Sig
Syntactic postdominators plugin.
Postdominators using value analysis results.
module Security : sig ... end
Security analysis.
module type INOUTKF = sig ... end
Signature common to some Inout plugin options. The results of the computations are available on a per function basis.
module type INOUT = sig ... end
Signature common to inputs and outputs computations. The results are also available on a per-statement basis.
module Inputs : sig ... end
State_builder.of read inputs. That is over-approximation of zones read by each function.
module Outputs : sig ... end
State_builder.of outputs. That is over-approximation of zones written by each function.
module Operational_inputs : sig ... end
State_builder.of operational inputs. That is:
This function should be called from time to time by all analysers taking time. In GUI mode, this will make the interface reactive.
val on_progress :
?debounced:int ->
?on_delayed:(int -> unit) ->
?on_finished:(unit -> unit) ->
(unit -> unit) ->
daemon
on_progress ?debounced ?on_delayed trigger
registers trigger
as new daemon to be executed on each yield
.
val off_progress : daemon -> unit
Unregister the daemon
.
val while_progress :
?debounced:int ->
?on_delayed:(int -> unit) ->
?on_finished:(unit -> unit) ->
(unit -> bool) ->
unit
while_progress ?debounced ?on_delayed ?on_finished trigger
is similar to on_progress
but the daemon is automatically unregistered as soon as trigger
returns false
. Same optional parameters than on_progress
.
val with_progress :
?debounced:int ->
?on_delayed:(int -> unit) ->
?on_finished:(unit -> 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. Same optional parameters than on_progress
.
Trigger all registered daemons (debounced). This function should be called from time to time by all analysers taking time. In GUI or Server mode, this will make the clients responsive.
Interrupt the currently running job: the next call to yield
will raise a Cancel
exception.
Pauses the currently running process for the specified time, in milliseconds. Registered daemons, if any, will be regularly triggered during this waiting time at a reasonable period with respect to their debouncing constraints.
This exception may be raised by yield
to interrupt computations.