package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Database in which static plugins are registered.

Modules providing general services:

Other main kernel modules:

Registering

val register : 'a ref -> 'a -> unit

Plugins must register values with this function.

val register_compute : string -> State.t list -> (unit -> unit) ref -> (unit -> unit) -> State.t
val register_guarded_compute : (unit -> bool) -> (unit -> unit) ref -> (unit -> unit) -> unit
  • before 26.0-Iron

    there was a string parameter (first position) that was only used for Journalization, that has been removed.

module Main : sig ... end

Frama-C main interface.

module Toplevel : sig ... end

Values

module Value : sig ... end

Deprecated module: use the Eva.mli API instead.

module From : sig ... end

Functional dependencies between function inputs and function outputs.

Plugins

module PostdominatorsTypes : sig ... end

Declarations common to the various postdominators-computing modules

Syntactic postdominators plugin.

Postdominators using value analysis results.

module Security : sig ... end

Security analysis.

module type INOUTKF = sig ... end

Signature common to some Inout plugin options. The results of the computations are available on a per function basis.

module type INOUT = sig ... end

Signature common to inputs and outputs computations. The results are also available on a per-statement basis.

module Inputs : sig ... end

State_builder.of read inputs. That is over-approximation of zones read by each function.

module Outputs : sig ... end

State_builder.of outputs. That is over-approximation of zones written by each function.

module Operational_inputs : sig ... end

State_builder.of operational inputs. That is:

GUI

val progress : (unit -> unit) ref

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

  • deprecated

    21.0-Scandium

type daemon

Registered daemon on progress.

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

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

  • parameter debounced

    the least amount of time between two successive calls to the daemon, in milliseconds (default is 0ms).

  • parameter on_delayed

    callback is invoked as soon as the time since the last yield is greater than debounced milliseconds (or 100ms at least).

  • parameter on_finished

    callback is invoked when the callback is unregistered.

val off_progress : daemon -> unit

Unregister the daemon.

val while_progress : ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) -> (unit -> bool) -> unit

while_progress ?debounced ?on_delayed ?on_finished trigger is similar to on_progress but the daemon is automatically unregistered as soon as trigger returns false. Same optional parameters than on_progress.

val with_progress : ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> 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. Same optional parameters than on_progress.

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 or Server mode, this will make the clients responsive.

val cancel : unit -> unit

Interrupt the currently running job: the next call to yield will raise a Cancel exception.

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 yield to interrupt computations.