Add tests for protect-call (generate and compile)

plugins/qcheck-stm/test/dune

@@ -42,3 +42,61 @@
  (alias runtest)
  (action
   (diff dune.inc dune.inc.gen)))
+
+; include dependency is not handle by dune_gen
+
+(library
+ (name protect_with)
+ (modules protect_with))
+
+(rule
+ (target protect_with_stm_tests.ml)
+ (package ortac-qcheck-stm)
+ (deps
+  (package ortac-core)
+  (package ortac-qcheck-stm))
+ (action
+  (setenv
+   ORTAC_ONLY_PLUGIN
+   qcheck-stm
+   (with-stderr-to
+    protect_with_errors
+    (run
+     ortac
+     qcheck-stm
+     %{dep:protect_with.mli}
+     "make ()"
+     "int t"
+     --include=protect_with_include
+     --protect-call=run_tests
+     -o
+     %{target})))))
+
+(test
+ (name protect_with_stm_tests)
+ (package ortac-qcheck-stm)
+ (modules protect_with_stm_tests protect_with_include)
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-multicoretests-util
+  ortac-runtime
+  protect_with)
+ (action
+  (echo
+   "\n%{dep:protect_with_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (action
+  (progn
+   (diff protect_with_errors.expected protect_with_errors)
+   (diff protect_with_stm_tests.expected.ml protect_with_stm_tests.ml))))
+
+(rule
+ (alias launchtests)
+ (action
+  (run %{dep:protect_with_stm_tests.exe} -v)))

plugins/qcheck-stm/test/protect_with.ml

@@ -0,0 +1,13 @@
+type 'a t = 'a list ref
+
+exception Empty
+
+let make () = ref []
+let push a t = t := a :: !t
+
+let pop t =
+  match !t with
+  | [] -> raise Empty
+  | x :: xs ->
+      t := xs;
+      x

plugins/qcheck-stm/test/protect_with.mli

@@ -0,0 +1,22 @@
+type 'a t
+(*@ mutable model contents : 'a sequence *)
+
+exception Empty
+
+val make : unit -> 'a t
+(*@ t = make ()
+    ensures t.contents = Sequence.empty *)
+
+val push : 'a -> 'a t -> unit
+(*@ push a t
+    modifies t.contents
+    ensures t.contents = Sequence.cons a (old t.contents) *)
+
+val pop : 'a t -> 'a
+(*@ a = pop t
+    modifies t.contents
+    ensures t.contents = if old t.contents = Sequence.empty
+                         then Sequence.empty
+                         else Sequence.tl (old t.contents)
+    ensures (old t.contents) = Sequence.cons a t.contents
+    raises Empty -> old t.contents = Sequence.empty = t.contents *)

plugins/qcheck-stm/test/protect_with_include.ml

@@ -0,0 +1 @@
+let run_tests tests = tests ()

plugins/qcheck-stm/test/protect_with_stm_tests.expected.ml

@@ -0,0 +1,193 @@
+(* This file is generated by ortac qcheck-stm,
+   edit how you run the tool instead *)
+open Protect_with
+module Spec =
+  struct
+    open STM
+    [@@@ocaml.warning "-26-27"]
+    include Protect_with_include
+    type sut = int t
+    type cmd =
+      | Push of int 
+      | Pop 
+    let show_cmd cmd__001_ =
+      match cmd__001_ with
+      | Push a_1 -> Format.asprintf "%s %a" "push" (Util.Pp.pp_int true) a_1
+      | Pop -> Format.asprintf "%s" "pop"
+    type nonrec state = {
+      contents: int Ortac_runtime.Gospelstdlib.sequence }
+    let init_state =
+      let () = () in
+      {
+        contents =
+          (try Ortac_runtime.Gospelstdlib.Sequence.empty
+           with
+           | e ->
+               raise
+                 (Ortac_runtime.Partial_function
+                    (e,
+                      {
+                        Ortac_runtime.start =
+                          {
+                            pos_fname = "protect_with.mli";
+                            pos_lnum = 8;
+                            pos_bol = 268;
+                            pos_cnum = 293
+                          };
+                        Ortac_runtime.stop =
+                          {
+                            pos_fname = "protect_with.mli";
+                            pos_lnum = 8;
+                            pos_bol = 268;
+                            pos_cnum = 307
+                          }
+                      })))
+      }
+    let init_sut () = make ()
+    let cleanup _ = ()
+    let arb_cmd _ =
+      let open QCheck in
+        make ~print:show_cmd
+          (let open Gen in
+             oneof [(pure (fun a_1 -> Push a_1)) <*> int; pure Pop])
+    let next_state cmd__002_ state__003_ =
+      match cmd__002_ with
+      | Push a_1 ->
+          {
+            contents =
+              ((try
+                  Ortac_runtime.Gospelstdlib.Sequence.cons a_1
+                    state__003_.contents
+                with
+                | e ->
+                    raise
+                      (Ortac_runtime.Partial_function
+                         (e,
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "protect_with.mli";
+                                 pos_lnum = 13;
+                                 pos_bol = 479;
+                                 pos_cnum = 504
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "protect_with.mli";
+                                 pos_lnum = 13;
+                                 pos_bol = 479;
+                                 pos_cnum = 536
+                               }
+                           }))))
+          }
+      | Pop ->
+          {
+            contents =
+              ((try
+                  if
+                    state__003_.contents =
+                      Ortac_runtime.Gospelstdlib.Sequence.empty
+                  then Ortac_runtime.Gospelstdlib.Sequence.empty
+                  else
+                    Ortac_runtime.Gospelstdlib.Sequence.tl
+                      state__003_.contents
+                with
+                | e ->
+                    raise
+                      (Ortac_runtime.Partial_function
+                         (e,
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "protect_with.mli";
+                                 pos_lnum = 18;
+                                 pos_bol = 719;
+                                 pos_cnum = 744
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "protect_with.mli";
+                                 pos_lnum = 20;
+                                 pos_bol = 824;
+                                 pos_cnum = 882
+                               }
+                           }))))
+          }
+    let precond cmd__010_ state__011_ =
+      match cmd__010_ with | Push a_1 -> true | Pop -> true
+    let postcond cmd__004_ state__005_ res__006_ =
+      let new_state__007_ = lazy (next_state cmd__004_ state__005_) in
+      match (cmd__004_, res__006_) with
+      | (Push a_1, Res ((Unit, _), _)) -> true
+      | (Pop, Res ((Result (Int, Exn), _), a_2)) ->
+          (match a_2 with
+           | Ok a_2 ->
+               (try
+                  state__005_.contents =
+                    (Ortac_runtime.Gospelstdlib.Sequence.cons a_2
+                       (Lazy.force new_state__007_).contents)
+                with
+                | e ->
+                    raise
+                      (Ortac_runtime.Partial_function
+                         (e,
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "protect_with.mli";
+                                 pos_lnum = 21;
+                                 pos_bol = 883;
+                                 pos_cnum = 895
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "protect_with.mli";
+                                 pos_lnum = 21;
+                                 pos_bol = 883;
+                                 pos_cnum = 940
+                               }
+                           })))
+           | Error (Empty) ->
+               (try
+                  let __t1__008_ =
+                    state__005_.contents =
+                      Ortac_runtime.Gospelstdlib.Sequence.empty in
+                  let __t2__009_ =
+                    Ortac_runtime.Gospelstdlib.Sequence.empty =
+                      (Lazy.force new_state__007_).contents in
+                  __t1__008_ && __t2__009_
+                with
+                | e ->
+                    raise
+                      (Ortac_runtime.Partial_function
+                         (e,
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "protect_with.mli";
+                                 pos_lnum = 22;
+                                 pos_bol = 941;
+                                 pos_cnum = 961
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "protect_with.mli";
+                                 pos_lnum = 22;
+                                 pos_bol = 941;
+                                 pos_cnum = 1005
+                               }
+                           })))
+           | _ -> false)
+      | _ -> true
+    let run cmd__012_ sut__013_ =
+      match cmd__012_ with
+      | Push a_1 -> Res (unit, (push a_1 sut__013_))
+      | Pop -> Res ((result int exn), (protect (fun () -> pop sut__013_) ()))
+  end
+module STMTests = (STM_sequential.Make)(Spec)
+let _ =
+  Spec.run_tests
+    (fun () ->
+       QCheck_base_runner.run_tests_main
+         (let count = 1000 in
+          [STMTests.agree_test ~count ~name:"Protect_with STM tests"]))