diff --git a/share/Makefile.common b/share/Makefile.common
index aa38332b7033d822be1a6ee7a67cfb582c02fd74..07e1d9b48211a70f3d5164642a17944ca7d7ed1b 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
@@ -84,7 +84,10 @@ 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-40-41-42-44-45-48-50
+# - 67 (unused module parameter in functor signature): naming all parameters
+# in functor signatures is a common practice that seems harmless. Warning 60
+# ensures that named functor parameters are indeed used in the implementation.
+WARNINGS ?= -w +a-4-6-9-40-41-42-44-45-48-50-67
# - 3 (deprecated feature) cannot always be avoided for OCaml stdlib when
# supporting several OCaml versions
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 8a4be465d70e99096ca0c79e586c87ef9486dff3..e8fa630ffafd76c910a589aa7206d936a3b98eb0 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -888,7 +888,8 @@ struct
C.error loc "not a C type"
let logic_type ctxt loc env t =
- let module C = struct end in (* force calls to go through ctxt *)
+ (* force calls to go through ctxt *)
+ let module [@warning "-60"] C = struct end in
let ltype t = ctxt.logic_type ctxt loc env t in
let ctype t = ltype t |> c_type_of loc in
match t with
@@ -2361,7 +2362,7 @@ struct
C.error t.term_loc "expecting a term that can be coerced to a boolean"
let rec normalize_update_term ctxt env loc t v =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
function
(* Transform terms like {x \with .c[idx] = v}
into {x \with .c = {x.c \with [idx] = v}}.
@@ -2405,7 +2406,7 @@ struct
idx_typing env loc t normalizing_cont toff
end
and normalize_update_cont ctxt env loc t =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
function
| [],_ -> assert false (* parsing invariant *)
| _,[] -> assert false (* parsing invariant *)
@@ -3173,7 +3174,7 @@ struct
(Pretty_utils.pp_list ~sep:",@ " Cil_printer.pp_logic_type) tl
and type_int_term ctxt env t =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
let tt = ctxt.type_term ctxt env t in
if not (plain_integral_type tt.term_type) then
ctxt.error t.lexpr_loc
@@ -3181,7 +3182,7 @@ struct
tt
and type_bool_term ctxt env t =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
let tt = ctxt.type_term ctxt env t in
if not (plain_boolean_type tt.term_type) then
ctxt.error t.lexpr_loc "boolean expected but %a found"
@@ -3189,14 +3190,14 @@ struct
mk_cast tt (Ltype (ctxt.find_logic_type Utf8_logic.boolean,[]))
and type_num_term_option ctxt env t =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
match t with
None -> None, Linteger (* Warning: should be an hybrid of integer
and float. *)
| Some t -> let t = type_num_term ctxt env t in Some t, t.term_type
and type_num_term ctxt env t =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
let tt = ctxt.type_term ctxt env t in
if not (is_arithmetic_type tt.term_type) then
ctxt.error t.lexpr_loc "integer or float expected";
@@ -3245,7 +3246,7 @@ struct
| _ -> [], ctxt.type_predicate ctxt env p0
let term_lval_assignable ctxt ~accept_formal env t =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
let t = ctxt.type_term ctxt env t in
if not (check_lval_kind { lval_assignable_mode with accept_formal } t) then
ctxt.error t.term_loc "not an assignable left value: %a"
@@ -3253,7 +3254,7 @@ struct
lift_set (term_lval (fun _ t -> t)) t
let term ctxt env t =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
match t.lexpr_node with
| PLnamed(name,t) ->
let t = ctxt.type_term ctxt env t in
@@ -3263,7 +3264,7 @@ struct
{ term_node = t'; term_loc=t.lexpr_loc; term_type=ty; term_name = [] }
let predicate ctxt env p0 =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
let loc = p0.lexpr_loc in
let predicate = ctxt.type_predicate ctxt in
let term = ctxt.type_term ctxt in
@@ -3442,7 +3443,7 @@ struct
ctxt.error loc "expecting a predicate and not tsets"
let type_from ctxt ~accept_formal env (l,d) =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
(* Yannick: [assigns *\at(\result,Post)] should be allowed *)
let tl =
term_lval_assignable ctxt ~accept_formal env l
@@ -3465,7 +3466,7 @@ struct
(tl, Cil_types.From tf)
let type_assign ctxt ~accept_formal env a =
- let module C = struct end in
+ let module [@warning "-60"] C = struct end in
match a with
WritesAny -> Cil_types.WritesAny
| Writes l ->
diff --git a/src/libraries/utils/hook.ml b/src/libraries/utils/hook.ml
index c8a1ea7c6e231a2dbbdc2b3b3fa1b38312d5cc1e..fd86d98d149804f623388ba489689bbd5ce3ed44 100644
--- a/src/libraries/utils/hook.ml
+++ b/src/libraries/utils/hook.ml
@@ -87,7 +87,7 @@ struct
let length () = Queue.length hooks
end
-module Make(X:sig end) = Build(struct type t = unit end)
+module Make() = Build(struct type t = unit end)
module Make_graph
(P: sig module Id:Comparable type param type result end)
diff --git a/src/libraries/utils/hook.mli b/src/libraries/utils/hook.mli
index 945e5baef4450bd034980a14812af305e9d13e27..dccab681241d987cdea6072125515b50838a4afb 100644
--- a/src/libraries/utils/hook.mli
+++ b/src/libraries/utils/hook.mli
@@ -92,7 +92,7 @@ module type Iter_hook = S with type result = unit
module Build(P:sig type t end) : Iter_hook with type param = P.t
(** Make a new empty hook from [unit]. *)
-module Make(X:sig end) : S with type param = unit and type result = unit
+module Make() : S with type param = unit and type result = unit
module Fold(P: sig type t end): S with type param = P.t and type result = P.t
diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.ml b/src/plugins/e-acsl/src/libraries/gmp_types.ml
index 84bbe038d874b982bca2792335ce09ac9fffc956..2aa16a7b580ce501db2645486833046ce50bd6ef 100644
--- a/src/plugins/e-acsl/src/libraries/gmp_types.ml
+++ b/src/plugins/e-acsl/src/libraries/gmp_types.ml
@@ -42,7 +42,7 @@ module type S = sig
val is_t: typ -> bool
end
-module Make(X: sig end) = struct
+module Make() = struct
let t_torig_ref = mk_dummy_type_info_ref ()
let t_struct_torig_ref = mk_dummy_type_info_ref ()
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index ea48d5ad04b302cde1962649b6154f0c8b2e16db..fa37b1b2e8c26db81e648d24506115ac47358a57 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -646,7 +646,9 @@ module Callwise = struct
Inout_type.map (Zone.filter_base filter) with_internals
with Not_found -> Inout_type.bottom
end) in
- let module Compute = Dataflows.Simple_forward(Fenv)(Computer) in
+ let module [@warning "-60"] Compute =
+ Dataflows.Simple_forward (Fenv) (Computer)
+ in
Computer.end_dataflow ()
let record_for_callwise_inout ((call_stack: Db.Value.callstack), value_res) =
@@ -715,7 +717,9 @@ module FunctionWise = struct
call_stack;
Stack.push kf call_stack;
- let module Compute = Dataflows.Simple_forward(Fenv)(Computer) in
+ let module [@warning "-60"] Compute =
+ Dataflows.Simple_forward (Fenv) (Computer)
+ in
let result = Computer.end_dataflow () in
ignore (Stack.pop call_stack);
result
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 7406f3753ddcdd15481c6defa1d9e2a36c403c12..fa69cac6e2aed1fe40f55c0fccefbcc417b4b221 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -76,9 +76,9 @@ module Make_Minimal
let reduce_further _sttae _expr _value = []
module Transfer
- (Valuation: Abstract_domain.Valuation with type value = value
- and type origin = origin
- and type loc = location)
+ (_: Abstract_domain.Valuation with type value = value
+ and type origin = origin
+ and type loc = location)
= struct
let update _valuation state = `Value state
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index e78644f8c489b4125db88289516e89dec38bc0f3..bbc3d74c956474204929ef2a28b1901e146ab709 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -62,8 +62,8 @@ module Make
let reduce_further _ _ _ = []
module Transfer
- (Valuation: Abstract_domain.Valuation with type value = value
- and type loc = location)
+ (_: Abstract_domain.Valuation with type value = value
+ and type loc = location)
= struct
let update _ _ = `Value ()
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index b0ac5fda287de708f60051d6f0da7013a440e9d3..96bced78522acc52b351e9dc1502e87d32ef3a95 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -95,7 +95,7 @@ module Make_Dataflow
(* --- Abstract values storage --- *)
- module Partition = Trace_partitioning.Make (Abstract) (Transfer) (AnalysisParam)
+ module Partition = Trace_partitioning.Make (Abstract) (AnalysisParam)
type store = Partition.store
type flow = Partition.flow
diff --git a/src/plugins/value/partitioning/trace_partitioning.ml b/src/plugins/value/partitioning/trace_partitioning.ml
index 336e75f30ac705dc23c7a9f9fe167c939856666b..0f9823d356a0b2e8c4a5e08b0d780cb4690f1f70 100644
--- a/src/plugins/value/partitioning/trace_partitioning.ml
+++ b/src/plugins/value/partitioning/trace_partitioning.ml
@@ -26,7 +26,6 @@ open Partition
module Make
(Abstract: Abstractions.Eva)
- (Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
(Kf : sig val kf: kernel_function end) =
struct
module Parameters = Partitioning_parameters.Make (Kf)
diff --git a/src/plugins/value/partitioning/trace_partitioning.mli b/src/plugins/value/partitioning/trace_partitioning.mli
index 584134d4d145952e501942657a1b92985b788e11..c33c38acb4a80d79379cdca55dc26fcb51f05a01 100644
--- a/src/plugins/value/partitioning/trace_partitioning.mli
+++ b/src/plugins/value/partitioning/trace_partitioning.mli
@@ -24,7 +24,6 @@ open Bottom.Type
module Make
(Abstract : Abstractions.Eva)
- (Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
(Kf : sig val kf: Cil_types.kernel_function end) :
sig
type state = Abstract.Dom.t (** The states being partitioned *)
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index c6dd04ab1c1280da7ee2927723be8bf6493c7f85..c30e307d2f8911f058c1b34ea4bf1e4e47bbc596 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -36,7 +36,7 @@ module type Key = sig
val tag: 'a key -> int
end
-module Make (X : sig end) = struct
+module Make () = struct
type 'a key = { tag: int;
name: string }
@@ -59,9 +59,9 @@ module Make (X : sig end) = struct
let print fmt x = Format.pp_print_string fmt x.name
end
-module Key_Value = Make (struct end)
-module Key_Location = Make (struct end)
-module Key_Domain = Make (struct end)
+module Key_Value = Make ()
+module Key_Location = Make ()
+module Key_Domain = Make ()
module type Shape = sig
include Key
diff --git a/src/plugins/value/utils/structure.mli b/src/plugins/value/utils/structure.mli
index c04eb8cda7bb222f5b24d2bdfc1a63de1e6214f5..e3b3e7988dd773f0b9fd59314f8e56aac663e2a5 100644
--- a/src/plugins/value/utils/structure.mli
+++ b/src/plugins/value/utils/structure.mli
@@ -41,7 +41,7 @@ module type Key = sig
val tag: 'a key -> int
end
-module Make (X : sig end) : Key
+module Make () : Key
(** Keys module for the abstract values of Eva. *)
module Key_Value : Key
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 5b9e54a4366c72f7bb67221e95d61d953d510e98..3fde0d76ebc9cc5324d2e3f06993c4a0734bb00c 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -242,7 +242,7 @@ module MakeCompiler(M:Sigs.Model) = struct
module M = M
module C = CodeSemantics.Make(M)
module L = LogicSemantics.Make(M)
- module A = LogicAssigns.Make(M)(C)(L)
+ module A = LogicAssigns.Make(M)(L)
end
module Comp_Region = MakeCompiler(Register(Static)(MemRegion))
diff --git a/src/plugins/wp/LogicAssigns.ml b/src/plugins/wp/LogicAssigns.ml
index 8da52bbfe3284f24683773458023027af7e55c15..fe9eab80a7ce01c0d132c125dd09933c64dd5eb1 100644
--- a/src/plugins/wp/LogicAssigns.ml
+++ b/src/plugins/wp/LogicAssigns.ml
@@ -24,7 +24,6 @@ open Sigs
module Make
( M : Sigs.Model )
- ( C : Sigs.CodeSemantics with module M = M )
( L : Sigs.LogicSemantics with module M = M ) =
struct
diff --git a/src/plugins/wp/LogicAssigns.mli b/src/plugins/wp/LogicAssigns.mli
index 92cd1d2006bb61cfbbe5f75ab8966db08f01d1c2..4ff9a6fb815eacb80e9e16244001a60062392260 100644
--- a/src/plugins/wp/LogicAssigns.mli
+++ b/src/plugins/wp/LogicAssigns.mli
@@ -22,6 +22,5 @@
module Make
( M : Sigs.Model )
- ( C : Sigs.CodeSemantics with module M = M )
( L : Sigs.LogicSemantics with module M = M ) :
Sigs.LogicAssigns with module M = M and module L = L