testing warnings

plugins/qcheck-stm/test/all_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/all_warnings_errors.expected

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

plugins/qcheck-stm/test/dune

@@ -1,3 +1,30 @@
+(cram
+ (package ortac-qcheck-stm)
+ (deps
+  (package ortac-core)
+  (package ortac-qcheck-stm)))
+
+(rule
+ (target all_warnings_errors)
+ (package ortac-qcheck-stm)
+ (deps
+  (package ortac-core)
+  (package ortac-qcheck-stm))
+ (action
+  (setenv
+   ORTAC_ONLY_PLUGIN
+   qcheck-stm
+   (ignore-stdout
+    (with-stderr-to
+     %{target}
+     (run ortac qcheck-stm %{dep:all_warnings.mli} "make 16 'a'" "char t"))))))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (action
+  (diff all_warnings_errors.expected all_warnings_errors)))
+
 (library
  (name array)
  (modules array))

plugins/qcheck-stm/test/test_errors.t

@@ -0,0 +1,120 @@
+In this file, we test the different ways to make the `ortac qcheck-stm`
+command-line fail.
+
+We can make a syntax error in either the expression for the `init` function, or
+in the type declaration for the sytem under test:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > val make : 'a -> 'a t
+  > EOF
+  $ ortac qcheck-stm foo.mli "" "int t"
+  Error: `' is not a well formed OCaml expression.
+
+  $ ortac qcheck-stm foo.mli "make 42" ""
+  Error: `' is not a well formed type expression.
+
+We can give a type that does not exist in the module as the system under test:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > EOF
+  $ ortac qcheck-stm foo.mli "()" "ty"
+  Error: Type `ty' is not declared in the module.
+
+We can forget to instatiate the type parameter of the system under test:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > val make : 'a -> 'a t
+  > EOF
+  $ ortac qcheck-stm foo.mli "make 42" "'a t"
+  Error: Type parameter `'a' should be instantiated.
+
+We can forget to specify the type of the system under test:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > EOF
+  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  File "foo.mli", line 1, characters 0-9:
+  Error: The type `t' given for the system under test is not specified.
+
+Or specify it without any model:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > (*@ ephemeral *)
+  > EOF
+  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  File "foo.mli", line 2, characters 3-14:
+  Error: The type `t' given for the system under test has no models.
+
+We can give a non-existing function for `init_state`:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > (*@ mutable model value : 'a *)
+  > EOF
+  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  Error: Function `make' is not declared in the module.
+
+We can forget to specify the function used for the `init_state` function:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > (*@ mutable model value : 'a list *)
+  > val make : 'a -> 'a t
+  > EOF
+  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  File "foo.mli", line 3, characters 0-21:
+  Error: The function `make' used for `init_state` is not approriately specified.
+
+Or specify it in a manner that does not allow to deduce the value of `state`:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > (*@ mutable model value : 'a list *)
+  > val make : 'a -> 'a t
+  > (*@ t = make a
+  >     requires true *)
+  > EOF
+  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  File "foo.mli", line 4, characters 3-33:
+  Error: The function ` t = make a
+      requires true ' used for `init_state` is not approriately specified.
+
+Or we van give a function that does not return the type of the system under test:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > (*@ mutable model value : 'a *)
+  > val make : int -> unit
+  > (*@ make i
+  >     modifies () *)
+  > EOF
+  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  File "foo.mli", line 3, characters 0-109:
+  Error: The function `make' used for `init_state` does not return `sut`.
+
+We are expected to give a function call as expression for the `init_state` function:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > (*@ mutable model value : 'a *)
+  > EOF
+  $ ortac qcheck-stm foo.mli "42" "int t"
+  Error: The expression `42
+  ' given for `init_state` is not a function call.
+
+It also does not support qualified names:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > (*@ mutable model value : 'a *)
+  > EOF
+  $ ortac qcheck-stm foo.mli "Bar.make 42" "int t"
+  Error: Qualified name (`Bar.make
+  ') is not supported yet for generating `init_state`.
+
+It checks the number of argument in the function call:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > (*@ mutable model value : 'a *)
+  > val make : 'a -> 'a t
+  > (*@ t = make a
+  >     ensures t.value = a *)
+  > EOF
+  $ ortac qcheck-stm foo.mli "make 42 73" "int t"
+  Error: Mismatch number of arguments between `make 42 73
+  ' and the function specification.
+