Test warnings triggering and display

Only the warnings of level warning (and not error) are tested in this
commit. The generated `.ml` file is ignored because it does not contain
relevant information and the OCaml compiler would complain about it.

plugins/qcheck-stm/test/dune

@@ -6,6 +6,10 @@
  (name hashtbl)
  (modules hashtbl))
 
+(library
+ (name testing_warnings)
+ (modules testing_warnings))
+
 (test
  (name array_stm_tests)
  (package ortac-qcheck-stm)
@@ -98,6 +102,26 @@
    (diff hashtbl_errors.expected hashtbl_errors)
    (diff hashtbl_stm_tests.expected.ml hashtbl_stm_tests.ml))))
 
+(rule
+ (target testing_warnings_errors)
+ (package ortac-qcheck-stm)
+ (deps
+  (package ortac-core)
+  (package ortac-wrapper)
+  (package ortac-monolith)
+  (package ortac-qcheck-stm))
+ (action
+  (ignore-stdout
+   (with-stderr-to
+    %{target}
+    (run ortac qcheck-stm %{dep:testing_warnings.mli} "make 16 'a'" "char t")))))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (action
+  (diff testing_warnings_errors.expected testing_warnings_errors)))
+
 (rule
  (alias launchtests)
  (action

plugins/qcheck-stm/test/testing_warnings.ml

@@ -0,0 +1,18 @@
+type 'a t = 'a array
+type s = A
+
+let make = Array.make
+let constant = ()
+let returning_sut a = Array.make 42 a
+let no_sut_argument = Fun.id
+let multiple_sut_argument _ _ = true
+let incompatible_type _ = true
+let no_spec _ = true
+let impossible_term_substitution _ = true
+let ignored_modified _ = ()
+let ensures_not_found_for_next_state _ = ()
+let type_not_supported _ = A
+let functional_argument _ _ = true
+let ghost_argument _ = true
+let ghost_returned_value _ = true
+let unsupported_quantification _ = true

plugins/qcheck-stm/test/testing_warnings.mli

@@ -0,0 +1,57 @@
+(*@ predicate p (x : 'a) = true *)
+
+type 'a t
+(*@ mutable model contents : 'a list *)
+
+type s
+
+val make : int -> 'a -> 'a t
+(*@ t = make i a
+    ensures t.contents = List.init i (fun x -> a) *)
+
+val constant : unit
+(*@ constant
+    ensures true *)
+
+val returning_sut : 'a -> 'a t
+(*@ t = returning_sut a *)
+
+val no_sut_argument : bool -> bool
+(*@ a = no_sut_argument b *)
+
+val multiple_sut_argument : 'a t -> 'a t -> bool
+(*@ b = multiple_sut_argument x y *)
+
+val incompatible_type : int t -> bool
+(*@ b = incompatible_type t *)
+
+val no_spec : 'a t -> bool
+(*@ b = no_spec t *)
+
+val impossible_term_substitution : 'a t -> bool
+(*@ impossible_term_substitution t
+    requires old t.contents = [] *)
+
+val ignored_modified : 'a t -> unit
+(*@ ignored_modified t
+    modifies () *)
+
+val ensures_not_found_for_next_state : 'a t -> unit
+(*@ ensures_not_found_for_next_state t
+    modifies t.contents *)
+
+val type_not_supported : 'a t -> s
+(*@ s = type_not_supported t *)
+
+val functional_argument : ('a -> bool) -> 'a t -> bool
+(*@ b = functional_argument p t *)
+
+val ghost_argument : 'a t -> bool
+(*@ b = ghost_argument [x : bool] t *)
+
+val ghost_returned_value : 'a t -> bool
+(*@ [ x : bool ], b = ghost_returned_value t *)
+
+val unsupported_quantification : 'a t -> bool
+(*@ b = unsupported_quantification t
+    ensures b = forall a. List.mem a t.contents -> p a *)

plugins/qcheck-stm/test/testing_warnings_errors.expected

@@ -0,0 +1,36 @@
+File "testing_warnings.mli", line 12, characters 0-138:
+Warning: `constant' is a constant.
+
+File "testing_warnings.mli", line 16, characters 26-30:
+Warning: `returning_sut' returns a sut.
+
+File "testing_warnings.mli", line 19, characters 22-34:
+Warning: `no_sut_argument' have no sut argument.
+
+File "testing_warnings.mli", line 22, characters 28-48:
+Warning: `multiple_sut_argument' have multiple sut arguments.
+
+File "testing_warnings.mli", line 25, characters 24-29:
+Warning: Type of system under test in `incompatible_type' is incompatible with command line argument.
+
+File "testing_warnings.mli", line 37, characters 13-15:
+Warning: Skipping `modifies` `(unit ):unit_1'.
+
+File "testing_warnings.mli", line 46, characters 27-37:
+Warning: Functional argument (`'a -> bool') are not tested.
+
+File "testing_warnings.mli", line 50, characters 24-25:
+Warning: Functions with a ghost argument (`x') are not tested.
+
+File "testing_warnings.mli", line 53, characters 6-7:
+Warning: Functions with a ghost returned value (`x_1') are not tested.
+
+File "testing_warnings.mli", line 4, characters 18-26:
+Warning: No translatable `ensures` clause found to generate `next_state` for model `contents'.
+
+File "testing_warnings.mli", line 57, characters 16-54:
+Warning: unsupported quantification. The clause has not been translated
+
+File "testing_warnings.mli", line 33, characters 17-18:
+Warning: The term `t_1:'a t' can not be substituted (supported only under `old` operator).
+