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"]))