Domain (frama-c-eva.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.