package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.1-Nickel.tar.gz

sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

doc/frama-c.kernel/Frama_c_kernel/Db/index.html

Module `Frama_c_kernel.Db`

Database in which static plugins are registered.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

Modules providing general services:

Dynamic: API for plug-ins linked dynamically
Log: message outputs and printers
Plugin: general services for plug-ins
Project and associated files: Datatype and State_builder.

Other main kernel modules:

Ast: the cil AST
Ast_info: syntactic value directly computed from the Cil Ast
File: Cil file initialization
Globals: global variables, functions and annotations
Annotations: annotations associated with a statement
Property_status: status of annotations
Kernel_function: C functions as seen by Frama-C
Stmts_graph: the statement graph
Loop: (natural) loops
Visitor: frama-c visitors
Kernel: general parameters of Frama-C (mostly set from the command line)

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

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 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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

On This Page

Registering
Plugins
1. GUI