Merge pull request #152 from n-osborne/next-state-wrn-msg

Adapt warning message for ensures not found

plugins/qcheck-stm/src/reserr.ml

@@ -130,9 +130,11 @@ let pp_kind ppf kind =
       pf ppf "Skipping unsupported modifies clause:@ %a" text
         "expected \"modifies x\" or \"modifies x.model\" where x is the SUT"
   | Ensures_not_found_for_next_state (f, m) ->
-      pf ppf "Skipping %s:@ model@ %s@ %a" f m text
-        "is declared as modified by the function but no translatable ensures \
-         clause was found"
+      pf ppf "Skipping %s:@ model@ %s %a@;%a%s%a" f m text
+        "is declared as modified by the function but no suitable ensures \
+         clause was found."
+        text "Specifications should contain at least one \"ensures x." m text
+        " = ...\" where x is the SUT"
   | Functional_argument f ->
       pf ppf "Skipping %s:@ %a" f text
         "functions are not supported yet as arguments"

plugins/qcheck-stm/test/all_warnings_errors.expected

@@ -51,8 +51,9 @@ File "all_warnings.mli", line 37, characters 13-23:
 37 |     modifies t.contents *)
                   ^^^^^^^^^^
 Warning: Skipping ensures_not_found_for_next_state: model contents is
-         declared as modified by the function but no translatable ensures
-         clause was found.
+         declared as modified by the function but no suitable ensures clause
+         was found. Specifications should contain at least one "ensures
+         x.contents = ..." where x is the SUT.
 File "all_warnings.mli", line 53, characters 16-54:
 53 |     ensures b = forall a. List.mem a t.contents -> p a *)
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^