Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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. The domains currently provided by Eva have priority ranging between 1 and 19, so a priority of 0 (respectively 20) ensures that a new domain is processed after (respectively before) the classic Eva domains. The 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 = Abstract.Context.External
module type Value = Abstract.Value.External
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.