[Kernel] Interpreted_automata: comments the dataflow functor.

src/kernel_services/analysis/interpreted_automata.mli

@@ -246,17 +246,33 @@ module UnrollUnnatural : sig
 end
 
 
-(* Dataflow computation *)
+(** Dataflow computation: simple data-flow analysis using interpreted automata.
+    This is mostly intended as an example for using interpreted automata;
+    see also tests/misc/interpreted_automata_dataflow.ml for a complete example
+    using this dataflow. *)
 
+(** Input domain for a simple dataflow analysis. *)
 module type Domain =
 sig
-  type t
+  type t (** States propagated by the dataflow analysis. *)
 
+  (** Merges two states coming from different paths. *)
   val join : t -> t -> t
-  val widen : t -> t -> t option (* returns None when inclusion *)
+
+  (** [widen v1 v2] must returns None if [v2] is included in [v1].
+      Otherwise, over-approximates the join between [v1] and [v2] such that
+      any sequence of successive widenings is ultimately stationary,
+      i.e. […widen (widen (widen x0 x1) x2) x3…] eventually returns None.
+      Called on loop heads to ensure the analysis termination. *)
+  val widen : t -> t -> t option
+
+  (** Transfer function for transitions: computes the state after the transition
+      from the state before. Returns None if the end of the transition is not
+      reachable from the given state. *)
   val transfer : vertex transition ->  t -> t option
 end
 
+(** Builds a simple dataflow analysis over an input domain. *)
 module Dataflow (D : Domain) :
 sig
   val fixpoint : Cil_types.kernel_function -> D.t -> D.t Vertex.Hashtbl.t

tests/misc/interpreted_automata_dataflow.i

@@ -2,6 +2,9 @@
 OPT: -load-script tests/misc/interpreted_automata_dataflow.ml
 */
 
+/* Tests the dataflow functor of interpreted automata via a caml script
+   implementing a propagation of constants. */
+
 void main(int x)
 {
   int y = 3;

tests/misc/interpreted_automata_dataflow.ml

@@ -33,7 +33,7 @@ struct
 
   exception Not_constant
 
-  let rec eval v exp = 
+  let rec eval v exp =
     match exp.enode with
     | Const (CInt64 (i,_,_)) ->
       (try Integer.to_int i with _ -> raise Not_constant)