Module Db

module Db: sig .. end

Database in which static plugins are registered.


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.

val register : 'a how_to_journalize -> 'a Stdlib.ref -> 'a -> unit

Plugins must register values with this function.

val register_compute : string ->
State.t list -> (unit -> unit) Stdlib.ref -> (unit -> unit) -> State.t
val register_guarded_compute : string ->
(unit -> bool) -> (unit -> unit) Stdlib.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.

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 

Syntactic postdominators plugin.

module PostdominatorsValue: PostdominatorsTypes.Sig 

Postdominators using value analysis results.

module RteGen: sig .. end

Runtime Error Annotation Generation 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.

GUI

val progress : (unit -> unit) Stdlib.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.