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-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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

Module `Frama_c_kernel.Async`

Module dedicated to asynchronous actions.

since 29.0-Copper

before 29.0-Copper
these features were in a module named Db

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.