Currently there is no protection against collisions between the namespaces of STM and of the user-provided code.
Here is a simple example, renaming the base type in ref.ml from t to ty, to match the base type in STM.
diff --git i/plugins/qcheck-stm/test/ref.ml w/plugins/qcheck-stm/test/ref.ml
index a105d98..c67cd35 100644
--- i/plugins/qcheck-stm/test/ref.ml
+++ w/plugins/qcheck-stm/test/ref.ml
@@ -1,4 +1,4 @@
-type t = int ref
+type ty = int ref
let make = ref
let get r = !r
diff --git i/plugins/qcheck-stm/test/ref.mli w/plugins/qcheck-stm/test/ref.mli
index 2cd26e7..9f37a5f 100644
--- i/plugins/qcheck-stm/test/ref.mli
+++ w/plugins/qcheck-stm/test/ref.mli
@@ -1,11 +1,11 @@
-type t = private int ref
+type ty = private int ref
(*@ mutable model value : integer *)
-val make : int -> t
+val make : int -> ty
(*@ r = make i
ensures r.value = i *)
-val get : t -> int
+val get : ty -> int
(*@ i = get r
pure
ensures i = r.value
The generated code fails to compile with the following error:
File "plugins/qcheck-stm/test/ref_stm_tests.ml", line 9, characters 15-17:
9 | type sut = ty
^^
Error: The type constructor ty expects 1 argument(s),
but is here applied to 0 argument(s)
Currently there is no protection against collisions between the namespaces of
STM
and of the user-provided code.Here is a simple example, renaming the base type in
ref.ml
fromt
toty
, to match the base type inSTM
.The generated code fails to compile with the following error: