Frama-C:
Plug-ins:
Libraries:

Frama-C API - Abstract_context

Signature of abstract state, which can be used to transfer information from states of abstract domains to abstract values.

An abstract context can be used to transfer information from the state of an abstract domain, in which an expression or lvalue is evaluated, to a value abstraction, which interprets operations during this evaluation. The context is built by the function build_context of abstract domains, and passed as argument of most transfer functions from Abstract_value.

module type S = sig ... end
type 'c key

Keys used to identify context modules.

module type Leaf = sig ... end

Signature for a leaf module of context.

type 'c dependencies =
  1. | Leaf : (module Leaf with type t = 'c) -> 'c dependencies
  2. | Node : 'l dependencies * 'r dependencies -> ('l * 'r) dependencies

Eva abstractions are divided between contexts, values, locations and domains. Values and domains depend on contexts, and use this type to declare such dependencies. In the standard case, a value or domain depends on a single context module Ctx and uses Leaf (module Ctx) to declare this dependency.