Adapt the warning message

ocaml-gospel · Oct 2, 2023 · e68ed72 · e68ed72
1 parent c722c12
commit e68ed72
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 7 deletions.
diff --git 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
@@ -115,6 +115,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 an expression \
+            containing it"
         (* 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
@@ -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
@@ -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
@@ -196,5 +196,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 an
+           expression containing it.