From 450384bc05450dc59cd309012078d11af55f5943 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Fri, 22 Sep 2023 13:29:50 +0200
Subject: [PATCH] Adapt the warning message

---
 plugins/qcheck-stm/src/reserr.ml      |  6 +++++-
 plugins/qcheck-stm/src/reserr.mli     |  2 +-
 plugins/qcheck-stm/src/stm_of_ir.ml   | 14 +++++++++++---
 plugins/qcheck-stm/test/test_errors.t |  4 ++--
 4 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml
index d26a702e..fa0b7952 100644
--- a/plugins/qcheck-stm/src/reserr.ml
+++ b/plugins/qcheck-stm/src/reserr.ml
@@ -25,7 +25,7 @@ type W.kind +=
   | Sut_type_not_specified of string
   | No_models of string
   | No_spec of string
-  | Impossible_term_substitution of [ `New | `Old | `NotModel ]
+  | Impossible_term_substitution of [ `Never | `New | `Old | `NotModel ]
   | Ignored_modifies
   | Ensures_not_found_for_next_state of (string * string)
   | Type_not_supported of string
@@ -116,6 +116,10 @@ let pp_kind ppf kind =
         | `NotModel ->
             "occurrences of the SUT in clauses are only supported to access \
              its model fields"
+        (* The  [`Never] case is used when generating [init_state] *)
+        | `Never ->
+            "impossible to define the value of the model with a recursive \
+             expression"
         (* The following cases should not be reported to the user at the moment
            (because they should be caught at some other points) *)
         | `Old ->
diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli
index ae2f948e..2b6ecff9 100644
--- a/plugins/qcheck-stm/src/reserr.mli
+++ b/plugins/qcheck-stm/src/reserr.mli
@@ -25,7 +25,7 @@ type W.kind +=
   | Sut_type_not_specified of string
   | No_models of string
   | No_spec of string
-  | Impossible_term_substitution of [ `New | `Old | `NotModel ]
+  | Impossible_term_substitution of [ `Never | `New | `Old | `NotModel ]
   | Ignored_modifies
   | Ensures_not_found_for_next_state of (string * string)
   | Type_not_supported of string
diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
index 0dff0ab2..c49e0005 100644
--- a/plugins/qcheck-stm/src/stm_of_ir.ml
+++ b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -88,11 +88,14 @@ let ocaml_of_term cfg t =
     occurrences of [gos_t] with [new_t] or [old_t] depending on whether the
     occurrence appears above or under the [old] operator, adding a [Lazy.force]
     if the corresponding [xxx_lz] is [true] (defaults to [false]). [gos_t] must
-    always be in a position in which it is applied to one of its model fields *)
+    always be in a position in which it is applied to one of its model fields.
+    Calling [subst_term] with [new_t] and [old_t] as None will check that the
+    term does not contain [gos_t] *)
 let subst_term state ~gos_t ?(old_lz = false) ~old_t ?(new_lz = false) ~new_t
     term =
   let exception
-    ImpossibleSubst of (Gospel.Tterm.term * [ `New | `Old | `NotModel ])
+    ImpossibleSubst of
+      (Gospel.Tterm.term * [ `Never | `New | `Old | `NotModel ])
   in
   let rec aux cur_lz cur_t term =
     let open Gospel.Tterm in
@@ -109,7 +112,12 @@ let subst_term state ~gos_t ?(old_lz = false) ~old_t ?(new_lz = false) ~new_t
               { term with t_node = Tfield (t, ls) }
           | None ->
               raise
-                (ImpossibleSubst (subt, if cur_t = new_t then `New else `Old))
+                (ImpossibleSubst
+                   ( subt,
+                     match (new_t, old_t) with
+                     | None, None -> `Never
+                     | None, _ -> `New
+                     | _, _ -> `Old ))
         else
           (* case x.f where f is _not_ a model field *)
           raise (ImpossibleSubst (term, `NotModel))
diff --git a/plugins/qcheck-stm/test/test_errors.t b/plugins/qcheck-stm/test/test_errors.t
index e1bd2696..e68a729e 100644
--- a/plugins/qcheck-stm/test/test_errors.t
+++ b/plugins/qcheck-stm/test/test_errors.t
@@ -205,5 +205,5 @@ We shouldn't be able to define a model by itsef in the `make` function:
   File "foo.mli", line 6, characters 22-23:
   6 |     ensures t.value = t.value *)
                             ^
-  Warning: Skipping clause: occurrences of the SUT in clauses are not supported
-           above old operator.
+  Warning: Skipping clause: impossible to define the value of the model with a
+           recursive expression.