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 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
Deprecated.21.0-Scandium

This function should be called from time to time by all analysers taking time. In GUI mode, this will make the interface reactive.

type daemon 

Registered daemon on progress.

val on_progress : ?debounced:int -> ?on_delayed:(int -> unit) -> (unit -> unit) -> daemon

on_progress ?debounced ?on_delayed trigger registers trigger as new daemon to be executed on each Db.yield.

debounced : the least amount of time between two successive calls to the daemon, in milliseconds (default is 0ms).
on_delayed : the callback invoked as soon as the time since the last Db.yield is greater than debounced milliseconds (or 100ms at least).
val off_progress : daemon -> unit

Unregister the daemon.

val flush : unit -> unit

Trigger all daemons immediately.

val yield : unit -> unit

Trigger all registered daemons (debounced). This function should be called from time to time by all analysers taking time. In GUI mode, this will make the interface reactive.

val cancel : unit -> unit

Interrupt the currently running job at the next call to Db.yield as a Cancel exception is raised.

val with_progress : ?debounced:int ->
?on_delayed:(int -> unit) -> (unit -> unit) -> ('a -> 'b) -> 'a -> 'b

with_progress ?debounced ?on_delayed trigger job data executes the given job on data while registering trigger as temporary (debounced) daemon. The daemon is finally unregistered at the end of the computation.

Illustrative example, where ... is the debounced time:

       job data :    |<-------------------------------------------------->|<daemon removed>
       yields   :       x   x  x x    x             x   x    x   xxx xxx
       trigger  :       |..........   |..........   |..........  |.........
       delayed  :                                   !
       notes    :      (1)           (2)           (3)
   
  1. First yield, normal trigger.
  2. Debounced yields leads to this second trigger.
  3. Delayed warning invoked since there was no yield for more than debounced period.

Raises every exception raised during the execution of job on data.

debounced : the least amount of time, in milliseconds, between two successive calls to the daemon (default is 0ms).
on_delayed : the callback invoked as soon as the time since the last yield is greater than debounced milliseconds (or 100ms at least).
val sleep : int -> unit

Pauses the currently running process for the specified time, in milliseconds. Registered daemons, if any, will be regularly triggered during this waiting time at a reasonable period with respect to their debouncing constraints.

exception Cancel

This exception may be raised by Db.yield to interrupt computations.