Frama-C:
Plug-ins:
Libraries:

Frama-C API - Abstract

Internal and External signature of abstractions used in the Eva engine.

Internal modules contains a structure value that describes the internal structure of the abstraction. This structure is used to automatically generate efficient accessors from a generic compound abstraction to specific leaf abstractions.

External modules export direct accessors to their leaf components. When a generic abstraction is a product of several specific abstractions, they allow interacting with each leaf abstraction identified by a key. Note that their behavior is undefined if an abstraction contains several times the same leaf module.

module Context : sig ... end

Key and structure for abstract contexts. See Structure for more details.

module Value : sig ... end

Key and structure for abstract values. See Structure for more details.

module Location : sig ... end

Key and structure for abstract locations. See Structure for more details.

module Domain : sig ... end

Key and structure for abstract domains. See Structure for more details.