diff --git a/src/kernel_services/analysis/interpreted_automata.mli b/src/kernel_services/analysis/interpreted_automata.mli
index dec17586091a3fdaa21f3862934ddd4490bf5c9d..e939c4cf6c4c86478c96343bfc7d689fa19d4713 100644
--- a/src/kernel_services/analysis/interpreted_automata.mli
+++ b/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
diff --git a/tests/misc/interpreted_automata_dataflow.i b/tests/misc/interpreted_automata_dataflow.i
index 0dbe0d1484555b607aa877ac49d051a0f09d4077..9446609755e0db82db642ed1331e1ec2ae8e9b6e 100644
--- a/tests/misc/interpreted_automata_dataflow.i
+++ b/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;
diff --git a/tests/misc/interpreted_automata_dataflow.ml b/tests/misc/interpreted_automata_dataflow.ml
index b23a0a3cd8de934cc94639302f490ec5bdd3da94..04843ba93f65bdc060783952b279b25231942995 100644
--- a/tests/misc/interpreted_automata_dataflow.ml
+++ b/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)