Skip to content

Commit

Permalink
Add tests for including the custom generators
Browse files Browse the repository at this point in the history
  • Loading branch information
n-osborne committed Mar 27, 2024
1 parent 651dcb0 commit 61cb3c9
Show file tree
Hide file tree
Showing 3 changed files with 28 additions and 0 deletions.
4 changes: 4 additions & 0 deletions plugins/qcheck-stm/test/array_config.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,3 +3,7 @@ open Array
let init_sut = make 16 'a'

type sut = char t

module Gen = struct
let int = small_signed_int
end
6 changes: 6 additions & 0 deletions plugins/qcheck-stm/test/array_stm_tests.expected.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,12 @@ module Ortac_runtime = Ortac_runtime_qcheck_stm
module Spec =
struct
open STM
module QCheck =
struct
include QCheck
module Gen = struct include Gen
let int = small_signed_int end
end
type sut = char t
type cmd =
| Length
Expand Down
18 changes: 18 additions & 0 deletions plugins/qcheck-stm/test/test_errors.t
Original file line number Diff line number Diff line change
Expand Up @@ -250,3 +250,21 @@ We shouldn't be able to define a model by itsef in the `make` function:
^
Warning: Skipping clause: impossible to define the initial value of the model
with a recursive expression.

If we add some custom generators, we should do so in a `Gen` module that is implemented (functor application or reference to another module are not supported):
$ cat > foo.mli << EOF
> type 'a t
> (*@ mutable model value : 'a *)
> val make : 'a -> 'a t
> (*@ t = make a
> ensures t.value = a *)
> EOF
$ cat > foo_config.ml << EOF
> module Gen = QCheck.Gen
> open Foo
> let init_sut = make 42 73
> type sut = int t
> EOF
$ ortac qcheck-stm foo.mli foo_config.ml
Error: Unsupported Gen module definition: only structures are allowed as
module definition here.

0 comments on commit 61cb3c9

Please sign in to comment.