From f97b5935184623ef6d9126adebcf0655e438cfb3 Mon Sep 17 00:00:00 2001
From: Nicolas Osborne <nicolas.osborne@tarides.com>
Date: Tue, 5 Mar 2024 16:36:15 +0100
Subject: [PATCH] Add cram tests on the effect of optional arguments

---
 .../qcheck-stm/test/test_optional_arguments.t | 32 +++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 plugins/qcheck-stm/test/test_optional_arguments.t

diff --git a/plugins/qcheck-stm/test/test_optional_arguments.t b/plugins/qcheck-stm/test/test_optional_arguments.t
new file mode 100644
index 00000000..26d56f2f
--- /dev/null
+++ b/plugins/qcheck-stm/test/test_optional_arguments.t
@@ -0,0 +1,32 @@
+In this file, we test the effect of the optional arguments of the command-line.
+
+  $ export ORTAC_ONLY_PLUGIN=qcheck-stm
+  $ 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" "int t" --include=mod | head
+  (* This file is generated by ortac qcheck-stm,
+     edit how you run the tool instead *)
+  open Foo
+  module Spec =
+    struct
+      open STM
+      [@@@ocaml.warning "-26-27"]
+      include Mod
+      type sut = int t
+      type cmd = |
+  $ ortac qcheck-stm foo.mli "make 42" "int t" --protect-call=protect | tail
+        match (cmd__004_, res__006_) with | _ -> true
+      let run cmd__010_ sut__011_ = match cmd__010_ with
+    end
+  module STMTests = (STM_sequential.Make)(Spec)
+  let _ =
+    Spec.protect
+      (fun () ->
+         QCheck_base_runner.run_tests_main
+           (let count = 1000 in
+            [STMTests.agree_test ~count ~name:"Foo STM tests"]))