package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install 

dune-project
 Dependency

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

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. P
    Pierre Nigron
  36. A
    Anne Pacalet
  37. V
    Valentin Perrelle
  38. G
    Guillaume Petiot
  39. D
    Dario Pinto
  40. V
    Virgile Prevosto
  41. A
    Armand Puccetti
  42. F
    Félix Ridoux
  43. V
    Virgile Robles
  44. J
    Jan Rochel
  45. M
    Muriel Roger
  46. J
    Julien Signoles
  47. N
    Nicolas Stouls
  48. K
    Kostyantyn Vorobyov
  49. B
    Boris Yakobowski

Maintainers

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

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

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.