[Eva] Comments abstract contexts, and removes unused functions.

src/plugins/eva/contexts/abstract_context.ml

@@ -20,23 +20,41 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** 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}. *)
+
 open Eval
 
 module type S = sig
-  include Datatype.S
+  type t
+
+  (** The default context used in a top abstract state, or if no domain has been
+      enabled — or no domain providing this context. *)
   val top : t
-  val is_included : t -> t -> bool
-  val join : t -> t -> t
+
+  (** In a product of abstract domains, merges the context provided by the
+      abstract state of each domain. *)
   val narrow : t -> t -> t or_bottom
 end
 
+(** Keys used to identify context modules. *)
 type 'c key = 'c Structure.Key_Context.key
 
+(** Signature for a leaf module of context. *)
 module type Leaf = sig
   include S
+
+  (** The key identifies the module and the type [t] of context. *)
   val key : t key
 end
 
+(** 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. *)
 type 'c dependencies =
   | Leaf : (module Leaf with type t = 'c) -> 'c dependencies
   | Node : 'l dependencies * 'r dependencies -> ('l * 'r) dependencies

src/plugins/eva/contexts/context_product.ml

@@ -21,9 +21,7 @@
 (**************************************************************************)
 
 module Make (L : Abstract_context.S) (R : Abstract_context.S) = struct
-  include Datatype.Pair (L) (R)
+  type t = L.t * R.t
   let top = (L.top, R.top)
-  let join (l, r) (l', r') = (L.join l l', R.join r r')
-  let is_included (l, r) (l', r') = L.is_included l l' && R.is_included r r'
   let narrow (l, r) (l', r') = Eval.Bottom.zip (L.narrow l l') (R.narrow r r')
 end

src/plugins/eva/contexts/unit_context.ml

@@ -20,9 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include Datatype.Unit
+type t = unit
 let top = ()
-let is_included () () = true
-let join () () = ()
 let narrow () () = `Value ()
 let key = Structure.Key_Context.create_key "Unit context"

src/plugins/eva/values/abstract_value.ml

@@ -46,12 +46,21 @@ type bound = Int of Integer.t | Float of float * fkind
 
 type pointer_comparison = Equality | Relation | Subtraction
 
+(** Enriched context.
+    This record could easily be extended to contain more information about the
+    context in which an evaluation takes place, if the need arises. *)
 type 'a enriched = { from_domains : 'a }
 
 (** Signature of abstract numerical values. *)
 module type S = sig
   include Datatype.S
 
+  (** A numerical value abstraction can optionally require some context from
+      abstract domains. Most transfer functions take the context as argument;
+      it is provided by the abstract state in which operations are performed.
+      See {!Abstract_context} for more details about contexts.
+      For values that don't need context, this type can be defined as unit
+      and the context argument can be safely ignored. *)
   type context
 
   val pretty_typ: typ option -> t Pretty_utils.formatter