From 1c5652464da5e2f71a24e2505d071e1dfd691411 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Mon, 9 Oct 2023 13:46:42 +0200 Subject: [PATCH] Adapt "ensures not found" warning message "translatable" was a bit confusing a word (translation was not really the issue). Add some explanation on what the ensures clause should look like. --- plugins/qcheck-stm/src/reserr.ml | 12 +++++++++--- plugins/qcheck-stm/test/all_warnings_errors.expected | 5 +++-- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml index d26a702e..a022cf3d 100644 --- a/plugins/qcheck-stm/src/reserr.ml +++ b/plugins/qcheck-stm/src/reserr.ml @@ -130,9 +130,15 @@ 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" diff --git a/plugins/qcheck-stm/test/all_warnings_errors.expected b/plugins/qcheck-stm/test/all_warnings_errors.expected index 5bd807a7..0da0b216 100644 --- a/plugins/qcheck-stm/test/all_warnings_errors.expected +++ b/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 *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^