Add test for returned tuple

ocaml-gospel · Jun 18, 2024 · d4c8ee3 · d4c8ee3
1 parent 1674f3c
commit d4c8ee3
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 0 deletions.
diff --git a/plugins/qcheck-stm/test/tuples.ml b/plugins/qcheck-stm/test/tuples.ml
@@ -3,3 +3,4 @@ include Hashtbl
 let create () = create ~random:false 10
 let add t (a, b) = add t a b
 let add' t (c, a, b) = if c then add t (a, b) else ()
+let size_tup t = (length t, length t)
diff --git a/plugins/qcheck-stm/test/tuples.mli b/plugins/qcheck-stm/test/tuples.mli
@@ -21,3 +21,8 @@ val add' : ('a, 'b) t -> bool * 'a * 'b -> unit
     ensures h.contents = match tup with c, a, b ->
         if c then (a, b) :: old h.contents
         else old h.contents *)
+
+val size_tup : ('a, 'b) t -> int * int
+(*@ x, y = size_tup t
+    ensures x = List.length t.contents
+    ensures y = List.length t.contents *)
diff --git a/plugins/qcheck-stm/test/tuples_errors.expected b/plugins/qcheck-stm/test/tuples_errors.expected
@@ -0,0 +1,4 @@
+File "tuples.mli", line 25, characters 29-38:
+25 | val size_tup : ('a, 'b) t -> int * int
+                                  ^^^^^^^^^
+Warning: Skipping size_tup: functions returning tuples are not supported yet.