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

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 Properties: sig .. end

Dealing with logical properties.

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.