package frama-c

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

Module Eva.Domain

Register new abstract domains.

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.