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 Users:sig
..end
module Properties:sig
..end
module PostdominatorsTypes:sig
..end
module Postdominators:PostdominatorsTypes.Sig
module PostdominatorsValue:PostdominatorsTypes.Sig
module RteGen:sig
..end
module Constant_Propagation:sig
..end
module Impact:sig
..end
module Security:sig
..end
module Pdg:sig
..end
module Sparecode:sig
..end
module Occurrence: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