From 295d64105a2f609a30c11abcb231099b9072c7c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 28 Jun 2024 17:26:48 +0200
Subject: [PATCH] [kernel] Interpreted automata: improves documentation of
 widening.

---
 .../analysis/interpreted_automata.mli                | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/kernel_services/analysis/interpreted_automata.mli b/src/kernel_services/analysis/interpreted_automata.mli
index e751f86f751..0fe34c38337 100644
--- a/src/kernel_services/analysis/interpreted_automata.mli
+++ b/src/kernel_services/analysis/interpreted_automata.mli
@@ -318,11 +318,17 @@ sig
   (** Merges two states coming from different paths. *)
   val join : t -> t -> t
 
-  (** [widen v1 v2] must returns None if [v2] is included in [v1].
-      Otherwise, over-approximates the join between [v1] and [v2] such that
+  (** [widen v1 v2] is called on loop heads after each iteration of the
+      analysis on the loop body: [v1] is the previous state before the
+      iteration, and [v2] the new state after the iteration.
+      The function must return None if the analysis has reached a fixpoint for
+      the loop: this is the case if [join v1 v2] is equivalent to [v1], as a new
+      iteration would have the same entry state as the last one.
+      Otherwise, it must return the new entry state for the next iteration,
+      by over-approximating 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. *)
+      This ensures the analysis termination. *)
   val widen : t -> t -> t option
 
   (** Transfer function for edges: computes the state after the transition
-- 
GitLab