Module Db
module Db: sig
.. end
Modules providing general services:
Other main kernel modules:
Ast
: the cil AST
Ast_info
: syntactic value directly computed from the Cil Ast
File
: Cil file initialization
Globals
: global variables, functions and annotations
Annotations
: annotations associated with a statement
Properties_status
: status of annotations
Kernel_function
: C functions as seen by Frama-C
Stmts_graph
: the statement graph
Loop
: (natural) loops
Visitor
: frama-c visitors
Kernel
: general parameters of Frama-C (mostly set from the command
line)
Registering
type 'a
how_to_journalize =
| |
Journalize of string * 'a Type.t |
| |
Journalization_not_required |
| |
Journalization_must_not_happen of string |
How to journalize the given function.
Since Beryllium-20090601-beta1
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
Change in Boron-20100401: now return the state of the computation.
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
Graphs
module Semantic_Callgraph: sig
.. end
Callgraph computed by value analysis.
Values
module Value: sig
.. end
The Value analysis itself.
module From: sig
.. end
Functional dependencies between function inputs and function outputs.
module Users: sig
.. end
Functions used by another function.
module Access_path: sig
.. end
Do not use yet.
Properties
module Properties: sig
.. end
Dealing with logical properties.
Plugins
module Syntactic_Callgraph: sig
.. end
Interface for the syntactic_callgraph plugin.
module PostdominatorsTypes: sig
.. end
Declarations common to the various postdominators-computing modules
module Postdominators: PostdominatorsTypes.Sig
Syntaxic postdominators plugin.
module PostdominatorsValue: PostdominatorsTypes.Sig
Postdominators using value analysis results.
module RteGen: sig
.. end
Runtime Error Annotation Generation plugin.
module Report: sig
.. end
Dump Properties-Status consolidation tree.
module Constant_Propagation: sig
.. end
Constant propagation plugin.
module Impact: sig
.. end
Impact analysis.
module Security: sig
.. end
Security analysis.
module Pdg: sig
.. end
Program Dependence Graph.
module Scope: sig
.. end
Interface for the Scope plugin.
module Sparecode: sig
.. end
Interface for the unused code detection.
module Occurrence: sig
.. end
Interface for the occurrence plugin.
module Slicing: sig
.. end
Interface for the slicing tool.
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.
GUI
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.
Consult the Plugin Development Guide for additional details.
exception Cancel
This exception may be raised by
Db.progress
to interrupt computations.