Frama-C API - Abstract_context
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 ... endtype 'c key = 'c Structure.Key_Context.keyKeys used to identify context modules.
module type Leaf = sig ... endSignature for a leaf module of context.
type 'c dependencies = | Leaf : (module Leaf with type t = 'c) -> 'c dependencies| 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.