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

Dependency

frama-c.com Edit opam file Versions (30)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-33.0-Arsenic.tar.gz

sha256=9c1cbffd28bb33c17a668107e39c96e4ae7378a3d8249f69b47afc7ee964e9b8

doc/frama-c-eva.core/Eva/Domain/index.html

Module `Eva.Domain`

type registered

Witness of the registration of an abstract domain, it can be used to programmatically enable the domain.

val register : 
  name:string ->
  descr:string ->
  ?experimental:bool ->
  ?priority:int ->
  ?auto_enable:(unit -> bool) ->
  (module Abstract_domain.Leaf) ->
  registered

Registers a leaf abstract domain.

name must be unique. The domain is enabled by -eva-domains name.
descr is a description printed in the help message of -eva-domains.
experimental is false by default. If set to true, a warning is emitted when the domain is enabled.
priority can be any integer; domains with higher priority are always processed first, and help messages list domains by decreasing priority. Current domains have priorities ranging from 1 to 10, so a priority of 0 (respectively 11) ensures that a domain is processed after (respectively before) the classic Eva domains. Default priority is 0.
auto_enable is called during domain configuration; if it returns true, the domain is automatically enabled. Always false by default.

val dynamic_register : 
  name:string ->
  descr:string ->
  ?experimental:bool ->
  ?priority:int ->
  ?auto_enable:(unit -> bool) ->
  (unit -> (module Abstract_domain.Leaf)) ->
  registered

Registers a dynamic domain, which is built at the start of an analysis analysis using the function given as last argument. See function register for more details.

module type Context = sig ... end

module type Value = sig ... end

module type Functor = sig ... end

Functor domain which can be built over any value abstractions, but with fixed locations dependencies.

val register_functor : 
  name:string ->
  descr:string ->
  ?experimental:bool ->
  ?priority:int ->
  ?auto_enable:(unit -> bool) ->
  (module Functor) ->
  registered

Registers a functor domain. See function register for more details.