Module Db

module Db: sig .. end
Database in which static plugins are registered.
Consult the Plugin Development Guide for additional details.


Modules providing general services: Other main kernel modules:

Registering


type 'a how_to_journalize = 
| Journalize of string * 'a Type.t (*
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 string (*
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.
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

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.

Properties


module Properties: sig .. end
Dealing with logical properties.

Plugins


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.