module Db:sig
..end
Database in which static plugins are registered.
Modules providing general services:
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
.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 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. | *) |
How to journalize the given function.
val register : 'a how_to_journalize -> 'a Pervasives.ref -> 'a -> unit
Plugins must register values with this function.
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
Frama-C main interface.
module Toplevel:sig
..end
module Value:sig
..end
The Value analysis itself.
module From:sig
..end
Functional dependencies between function inputs and function outputs.
module Properties:sig
..end
Dealing with logical properties.
module PostdominatorsTypes:sig
..end
Declarations common to the various postdominators-computing modules
module Postdominators:PostdominatorsTypes.Sig
Syntactic postdominators plugin.
module PostdominatorsValue:PostdominatorsTypes.Sig
Postdominators using value analysis results.
module RteGen:sig
..end
Runtime Error Annotation Generation plugin.
module Constant_Propagation:sig
..end
Constant propagation plugin.
module Security:sig
..end
Security analysis.
module Pdg:sig
..end
Program Dependence Graph.
module Sparecode:sig
..end
Interface for the unused code detection.
module type INOUTKF =sig
..end
Signature common to some Inout plugin options.
module type INOUT =sig
..end
module Inputs:sig
..end
State_builder.of read inputs.
module Outputs:sig
..end
State_builder.of outputs.
module Operational_inputs:sig
..end
State_builder.of operational inputs.
val progress : (unit -> unit) Pervasives.ref
This function should be called from time to time by all analysers taking time. In GUI mode, this will make the interface reactive.
exception Cancel
This exception may be raised by Db.progress
to interrupt computations.