Skip to content

Commit

Permalink
Add cram tests on the effect of optional arguments
Browse files Browse the repository at this point in the history
  • Loading branch information
n-osborne committed Mar 5, 2024
1 parent b90e23f commit f97b593
Showing 1 changed file with 32 additions and 0 deletions.
32 changes: 32 additions & 0 deletions plugins/qcheck-stm/test/test_optional_arguments.t
Original file line number Diff line number Diff line change
@@ -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"]))

0 comments on commit f97b593

Please sign in to comment.