Commit 25ecfd49 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[dev] silence warning 40 and 42

type-based disambiguation is not a bad thing after all.
parent 7633c48b
......@@ -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
......
......@@ -22,8 +22,6 @@
open Cil_types
[@@@ warning "-40"]
(* ---------------------------------------------------------------------- *)
(* --- Graph definition --- *)
(* ---------------------------------------------------------------------- *)
......
......@@ -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
......
......@@ -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
......
......@@ -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 () ->
......
......@@ -23,8 +23,6 @@
open Cil_types
open Logic_ptree
[@@@ warning "-42"]
type slevel_annotation =
| SlevelMerge
| SlevelDefault
......
......@@ -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"
......
(* test API of StmtSemantics *)
[@@@ warning "-40"]
[@@@ warning "-42"]
open Wp
open Factory
open Sigs
......
(* test API of StmtCompiler for relational property verification*)
[@@@ warning "-40"]
[@@@ warning "-42"]
open Wp
open Factory
open Sigs
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment