Merge branch 'feature/virgile/no-warn-40-42' into 'master'

[dev] silence warning 40 and 42

Closes #712

See merge request frama-c/frama-c!2495

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

src/kernel_services/analysis/interpreted_automata.ml

@@ -22,8 +22,6 @@
 
 open Cil_types
 
-[@@@ warning "-40"]
-
 (* ---------------------------------------------------------------------- *)
 (* --- Graph definition                                               --- *)
 (* ---------------------------------------------------------------------- *)

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

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

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 () ->

src/plugins/value/utils/partitioning_annots.ml

@@ -23,8 +23,6 @@
 open Cil_types
 open Logic_ptree
 
-[@@@ warning "-42"]
-
 type slevel_annotation =
   | SlevelMerge
   | SlevelDefault

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"
 

src/plugins/wp/tests/wp/stmtcompiler_test.ml

 (* test API of StmtSemantics *)
 
-[@@@ warning "-40"]
-[@@@ warning "-42"]
-
 open Wp
 open Factory
 open Sigs

src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml

 (* test API of StmtCompiler for relational property verification*)
 
-[@@@ warning "-40"]
-[@@@ warning "-42"]
-
 open Wp
 open Factory
 open Sigs