Frama-C API - `Abstractions`

Registration of abstract domains.

module Domain : sig ... end

Reduced product between value abstractions.

module Reducer : sig ... end

Value reduced product registration. Registering a value reduced product requires the keys of each value abstractions involved along with a reducer, i.e. a function that perform the reduction.

Configuration of an analysis.

module Config : sig ... end

Configuration defining the abstractions to be used in an analysis. A configuration is a set of registered abstract domains. Each domain comes with an optional analysis mode. None is the default mode: the domain is enabled for the whole analysis. See Domain_mode for more details.

Types and functions used in the engine.

module type Value_with_reduction = sig ... end

The value abstractions signature used in the engine, with the reduction function of the reduced product.

module type S = sig ... end

The four abstractions used in an Eva analysis.

val make : Config.t -> (module S)

Builds the abstractions according to a configuration.

Analysis low level modifications.

module Hooks : sig ... end