From 25ecfd491c6e409dd71d08c0b4468616aae54ccb Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 9 Jan 2020 10:37:38 +0100
Subject: [PATCH] [dev] silence warning 40 and 42
type-based disambiguation is not a bad thing after all.
---
share/Makefile.common | 9 ++++++---
src/kernel_services/analysis/interpreted_automata.ml | 2 --
src/libraries/utils/wto.ml | 2 --
src/plugins/value/domains/traces_domain.ml | 2 --
src/plugins/value/engine/iterator.ml | 3 ---
src/plugins/value/utils/partitioning_annots.ml | 2 --
src/plugins/wp/ProverWhy3.ml | 3 ---
src/plugins/wp/tests/wp/stmtcompiler_test.ml | 3 ---
src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml | 3 ---
9 files changed, 6 insertions(+), 23 deletions(-)
diff --git a/share/Makefile.common b/share/Makefile.common
index d89db19e691..aa38332b703 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
@@ -69,8 +69,11 @@ ifeq ($(DEVELOPMENT),yes)
# refactoring before being enabled.
# - 9 (missing field in record pattern) is much too heavy. Most of the time
# not all fields are relevant in pattern-matching Frama-C's AST.
-# - 41 (ambiguous constructor or label name) prevents type-based
-# disambiguation, a feature which is seen as a good thing by many developers
+# - 40 (constructor or label name used out of scope)
+# - 41 (ambiguous constructor or label name)
+# - 42 (Disambiguated constructor or label name)
+# these three warnings prevents type-based disambiguation,
+# a feature which is seen as a good thing by many developers
# - 44 (open shadows an identifier)
# - 45 (open shadows a label or constructor): While the use of open directives
# is supposed to stay small, it should still be possible to open modules
@@ -81,7 +84,7 @@ ifeq ($(DEVELOPMENT),yes)
# - 50 (warning about ambiguously placed OCamldoc comments): while it would be
# useful to ensure OCamldoc understands comments correctly, some clean-up
# is needed before enabling this warning.
-WARNINGS ?= -w +a-4-6-9-41-44-45-48-50
+WARNINGS ?= -w +a-4-6-9-40-41-42-44-45-48-50
# - 3 (deprecated feature) cannot always be avoided for OCaml stdlib when
# supporting several OCaml versions
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index a1159e205a6..418500d52f5 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -22,8 +22,6 @@
open Cil_types
-[@@@ warning "-40"]
-
(* ---------------------------------------------------------------------- *)
(* --- Graph definition --- *)
(* ---------------------------------------------------------------------- *)
diff --git a/src/libraries/utils/wto.ml b/src/libraries/utils/wto.ml
index 617ae52bb06..bf776d6fe33 100644
--- a/src/libraries/utils/wto.ml
+++ b/src/libraries/utils/wto.ml
@@ -53,8 +53,6 @@ let flatten wto =
in
List.rev (f [] wto)
-[@@@ warning "-42"]
-
(* Bourdoncle's WTO algorithm builds on Tarjan's SCC algorithm. In Tarjan:
- We visit every node once, starting from root, by following the
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index e12ed3ebeb3..c22c8bcfd19 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -31,8 +31,6 @@ module Frama_c_File = File
open Cil_types
open Cil_datatype
-[@@@ warning "-40-42"]
-
module Node : sig
include Datatype.S_with_collections
val id: t -> int
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index bae4fbcc7b3..b0ac5fda287 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -24,9 +24,6 @@ open Cil_types
open Interpreted_automata
open Bottom.Type
-[@@@warning "-42"]
-
-
let check_signals, signal_abort =
let signal_emitted = ref false in
(fun () ->
diff --git a/src/plugins/value/utils/partitioning_annots.ml b/src/plugins/value/utils/partitioning_annots.ml
index a4ee12b872f..804c3c8e15f 100644
--- a/src/plugins/value/utils/partitioning_annots.ml
+++ b/src/plugins/value/utils/partitioning_annots.ml
@@ -23,8 +23,6 @@
open Cil_types
open Logic_ptree
-[@@@ warning "-42"]
-
type slevel_annotation =
| SlevelMerge
| SlevelDefault
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index e9812047759..4fbae85bf44 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -20,9 +20,6 @@
(* *)
(**************************************************************************)
-(* Allow type-desambiguation for symbols *)
-[@@@ warning "-40-42"]
-
let dkey = Wp_parameters.register_category "prover"
let dkey_api = Wp_parameters.register_category "why3_api"
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index 265016e03e5..3e4c83b1b5d 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
@@ -1,8 +1,5 @@
(* test API of StmtSemantics *)
-[@@@ warning "-40"]
-[@@@ warning "-42"]
-
open Wp
open Factory
open Sigs
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 98a139cf92e..a474167455d 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -1,8 +1,5 @@
(* test API of StmtCompiler for relational property verification*)
-[@@@ warning "-40"]
-[@@@ warning "-42"]
-
open Wp
open Factory
open Sigs
--
GitLab