Merge pull request #139 from n-osborne/stm-add-warnings

Disable warnings in generated code
ocaml-gospel · Sep 20, 2023 · df2e81e · df2e81e
2 parents 5dc2443 + 0596857
commit df2e81e
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 4 deletions.
diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -759,6 +759,7 @@ let ghost_functions config =
 let stm config ir =
   let open Reserr in
   let* config, ghost_functions = ghost_functions config ir.ghost_functions in
+  let warn = [%stri [@@@ocaml.warning "-26-27"]] in
   let sut = sut_type config in
   let cmd = cmd_type ir in
   let* cmd_show = cmd_show ir in
@@ -784,6 +785,7 @@ let stm config ir =
     pmod_structure
       [
         open_mod "STM";
+        warn;
         sut;
         cmd;
         cmd_show;

diff --git a/plugins/qcheck-stm/test/array_stm_tests.expected.ml b/plugins/qcheck-stm/test/array_stm_tests.expected.ml
@@ -2,6 +2,7 @@ open Array
 module Spec =
   struct
     open STM
+    [@@@ocaml.warning "-26-27"]
     type sut = char t
     type cmd =
       | Length 

diff --git a/plugins/qcheck-stm/test/dune b/plugins/qcheck-stm/test/dune
@@ -45,7 +45,6 @@
   qcheck-multicoretests-util
   ortac-runtime
   array)
- (flags :standard -w -26-27-32-33)
  (action
   (echo
    "\n%{dep:array_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))
@@ -96,7 +95,6 @@
   qcheck-multicoretests-util
   ortac-runtime
   hashtbl)
- (flags :standard -w -23-26-27-32-33 -w -37)
  (action
   (echo
    "\n%{dep:hashtbl_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))
@@ -151,7 +149,6 @@
   qcheck-multicoretests-util
   ortac-runtime
   record)
- (flags :standard -w -27)
  (action
   (echo
    "\n%{dep:record_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))
@@ -199,7 +196,6 @@
   qcheck-multicoretests-util
   ortac-runtime
   ref)
- (flags :standard -w -27)
  (action
   (echo
    "\n%{dep:ref_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))

diff --git a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml
@@ -7,6 +7,7 @@ let rec remove_first x xs_1 =
 module Spec =
   struct
     open STM
+    [@@@ocaml.warning "-26-27"]
     type sut = (char, int) t
     type cmd =
       | Clear 

diff --git a/plugins/qcheck-stm/test/record_stm_tests.expected.ml b/plugins/qcheck-stm/test/record_stm_tests.expected.ml
@@ -2,6 +2,7 @@ open Record
 module Spec =
   struct
     open STM
+    [@@@ocaml.warning "-26-27"]
     type sut = t
     type cmd =
       | Get 

diff --git a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml
@@ -2,6 +2,7 @@ open Ref
 module Spec =
   struct
     open STM
+    [@@@ocaml.warning "-26-27"]
     type sut = t
     type cmd =
       | Get