diff --git a/configurator.ml b/configurator.ml
index 4bf225310fb71852fd541c89f62742c9065f17fc..7be17a56ace254186509392947520793a2d73a4b 100644
--- a/configurator.ml
+++ b/configurator.ml
@@ -59,7 +59,6 @@ module C_preprocessor = struct (* This could be put in Dune? *)
type t =
{ preprocessor: string
; pp_opt: string option
- ; is_gnu: bool
}
let stdout_contains out str =
@@ -97,24 +96,9 @@ module C_preprocessor = struct (* This could be put in Dune? *)
Temp.create ~dir ~suffix:".c" (fun name -> write_file name code) in
C.Process.run configurator ~dir preprocessor (options @ [ file ])
- let is_gnu configurator preprocessor =
- let code = {|#ifdef _FC_UNDEFINED_SYMBOL
-#error This should not remain after preprocessing
-#endif
-int kept_after_preprocessing = 42;
-|}
- in
- (* GNU preprocessors are always compatible with '-E'.
- For 'cpp', the '-E' flag is unnecessary, but still works. *)
- let result = call configurator preprocessor ["-E"] code in
- result.exit_code = 0 &&
- stdout_contains result.stdout "kept_after_preprocessing" &&
- not (stdout_contains result.stdout "should not remain")
-
let get configurator =
let preprocessor, pp_opt = find_preprocessor configurator in
- let is_gnu = is_gnu configurator preprocessor in
- { preprocessor ; pp_opt; is_gnu }
+ { preprocessor ; pp_opt }
let preprocess configurator t options code =
call configurator t.preprocessor (Option.to_list t.pp_opt @ options) code
diff --git a/dev/dune-workspace.bench b/dev/dune-workspace.bench
index 1f5ad5f7195c1c589acd1a37e04a56aa999a51c3..a4c42e207dd6c5096b61b4434a3c803323ca35ef 100644
--- a/dev/dune-workspace.bench
+++ b/dev/dune-workspace.bench
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/dev/dune-workspace.cover b/dev/dune-workspace.cover
index 86349742cd4e9d71bf7ee44ed42b70934fd3cf91..98a198201406e64560f57f798cb2078d4f6cb06c 100644
--- a/dev/dune-workspace.cover
+++ b/dev/dune-workspace.cover
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/doc/developer/dune-workspace.bench b/doc/developer/dune-workspace.bench
index 87e6d04e0ad58aba035cac6a3f7b7c68eda27674..8416a8f539d444aed0ea1f59196c2783dabd484f 100644
--- a/doc/developer/dune-workspace.bench
+++ b/doc/developer/dune-workspace.bench
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(context
(default
(name bench)
diff --git a/doc/developer/examples/acsl_extension_ext_types/dune-project b/doc/developer/examples/acsl_extension_ext_types/dune-project
index 5646419c5301bfc9204bb63e0d35fb73a2459762..58bd1e5c15ec9baaa10bfa8608d9966dca0aac59 100644
--- a/doc/developer/examples/acsl_extension_ext_types/dune-project
+++ b/doc/developer/examples/acsl_extension_ext_types/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-example)
diff --git a/doc/developer/examples/acsl_extension_foo/dune-project b/doc/developer/examples/acsl_extension_foo/dune-project
index 5646419c5301bfc9204bb63e0d35fb73a2459762..58bd1e5c15ec9baaa10bfa8608d9966dca0aac59 100644
--- a/doc/developer/examples/acsl_extension_foo/dune-project
+++ b/doc/developer/examples/acsl_extension_foo/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-example)
diff --git a/doc/developer/examples/callstack/dune-project b/doc/developer/examples/callstack/dune-project
index 5646419c5301bfc9204bb63e0d35fb73a2459762..58bd1e5c15ec9baaa10bfa8608d9966dca0aac59 100644
--- a/doc/developer/examples/callstack/dune-project
+++ b/doc/developer/examples/callstack/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-example)
diff --git a/doc/developer/examples/syntactic_check/dune-project b/doc/developer/examples/syntactic_check/dune-project
index 5646419c5301bfc9204bb63e0d35fb73a2459762..58bd1e5c15ec9baaa10bfa8608d9966dca0aac59 100644
--- a/doc/developer/examples/syntactic_check/dune-project
+++ b/doc/developer/examples/syntactic_check/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-example)
diff --git a/doc/developer/tutorial/hello/src/dune-project b/doc/developer/tutorial/hello/src/dune-project
index 1ceb1f524013c791e4c7f6892c9fe7684e5024cb..f4d53a0723768620f6bd9b2d38f64d44403a1324 100644
--- a/doc/developer/tutorial/hello/src/dune-project
+++ b/doc/developer/tutorial/hello/src/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/doc/developer/tutorial/hello/v1-simple/dune-project b/doc/developer/tutorial/hello/v1-simple/dune-project
index df0ab2a885a56ee655b69017390cbe479c05fbee..ed9003050122d5b61d407b7d4d0d2c71ee226530 100644
--- a/doc/developer/tutorial/hello/v1-simple/dune-project
+++ b/doc/developer/tutorial/hello/v1-simple/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-hello)
diff --git a/doc/developer/tutorial/hello/v2-register/dune-project b/doc/developer/tutorial/hello/v2-register/dune-project
index df0ab2a885a56ee655b69017390cbe479c05fbee..ed9003050122d5b61d407b7d4d0d2c71ee226530 100644
--- a/doc/developer/tutorial/hello/v2-register/dune-project
+++ b/doc/developer/tutorial/hello/v2-register/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-hello)
diff --git a/doc/developer/tutorial/hello/v3-log/dune-project b/doc/developer/tutorial/hello/v3-log/dune-project
index df0ab2a885a56ee655b69017390cbe479c05fbee..ed9003050122d5b61d407b7d4d0d2c71ee226530 100644
--- a/doc/developer/tutorial/hello/v3-log/dune-project
+++ b/doc/developer/tutorial/hello/v3-log/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-hello)
diff --git a/doc/developer/tutorial/hello/v4-options/dune-project b/doc/developer/tutorial/hello/v4-options/dune-project
index df0ab2a885a56ee655b69017390cbe479c05fbee..ed9003050122d5b61d407b7d4d0d2c71ee226530 100644
--- a/doc/developer/tutorial/hello/v4-options/dune-project
+++ b/doc/developer/tutorial/hello/v4-options/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-hello)
diff --git a/doc/developer/tutorial/hello/v5-multiple/dune-project b/doc/developer/tutorial/hello/v5-multiple/dune-project
index df0ab2a885a56ee655b69017390cbe479c05fbee..ed9003050122d5b61d407b7d4d0d2c71ee226530 100644
--- a/doc/developer/tutorial/hello/v5-multiple/dune-project
+++ b/doc/developer/tutorial/hello/v5-multiple/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-hello)
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/dune-project b/doc/developer/tutorial/hello/v6-test-with-bug/dune-project
index df0ab2a885a56ee655b69017390cbe479c05fbee..ed9003050122d5b61d407b7d4d0d2c71ee226530 100644
--- a/doc/developer/tutorial/hello/v6-test-with-bug/dune-project
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-hello)
diff --git a/doc/developer/tutorial/hello/v7-doc/dune-project b/doc/developer/tutorial/hello/v7-doc/dune-project
index df0ab2a885a56ee655b69017390cbe479c05fbee..ed9003050122d5b61d407b7d4d0d2c71ee226530 100644
--- a/doc/developer/tutorial/hello/v7-doc/dune-project
+++ b/doc/developer/tutorial/hello/v7-doc/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-hello)
diff --git a/doc/developer/tutorial/viewcfg/v1-simple/dune-project b/doc/developer/tutorial/viewcfg/v1-simple/dune-project
index f51b073e8f54f8f308c6d4ccd4f93156ad87be86..fea29a8a57b3ebf740a5340d6274c2c650d20a07 100644
--- a/doc/developer/tutorial/viewcfg/v1-simple/dune-project
+++ b/doc/developer/tutorial/viewcfg/v1-simple/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-view-cfg)
diff --git a/doc/developer/tutorial/viewcfg/v2-options/dune-project b/doc/developer/tutorial/viewcfg/v2-options/dune-project
index f51b073e8f54f8f308c6d4ccd4f93156ad87be86..fea29a8a57b3ebf740a5340d6274c2c650d20a07 100644
--- a/doc/developer/tutorial/viewcfg/v2-options/dune-project
+++ b/doc/developer/tutorial/viewcfg/v2-options/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-view-cfg)
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/dune-project b/doc/developer/tutorial/viewcfg/v3-eva/dune-project
index f51b073e8f54f8f308c6d4ccd4f93156ad87be86..fea29a8a57b3ebf740a5340d6274c2c650d20a07 100644
--- a/doc/developer/tutorial/viewcfg/v3-eva/dune-project
+++ b/doc/developer/tutorial/viewcfg/v3-eva/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-view-cfg)
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/dune-project b/doc/developer/tutorial/viewcfg/v4-bogue/dune-project
index f51b073e8f54f8f308c6d4ccd4f93156ad87be86..fea29a8a57b3ebf740a5340d6274c2c650d20a07 100644
--- a/doc/developer/tutorial/viewcfg/v4-bogue/dune-project
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-view-cfg)
diff --git a/doc/developer/tutorial/viewcfg/v5-state/dune-project b/doc/developer/tutorial/viewcfg/v5-state/dune-project
index f51b073e8f54f8f308c6d4ccd4f93156ad87be86..fea29a8a57b3ebf740a5340d6274c2c650d20a07 100644
--- a/doc/developer/tutorial/viewcfg/v5-state/dune-project
+++ b/doc/developer/tutorial/viewcfg/v5-state/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-view-cfg)
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/dune-project b/doc/developer/tutorial/viewcfg/v6-state-clear/dune-project
index f51b073e8f54f8f308c6d4ccd4f93156ad87be86..fea29a8a57b3ebf740a5340d6274c2c650d20a07 100644
--- a/doc/developer/tutorial/viewcfg/v6-state-clear/dune-project
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
(using dune_site 0.1)
(name frama-c-view-cfg)
diff --git a/dune-project b/dune-project
index 2882306b7d98cfa4b7d3adbd7e003ca3ed203a04..6dcfb7a66093e2a97ded1ace3e4e5bd25f4c140b 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/opam b/opam
index 0cfa34fd454e3ad3ec085f01f91609aa8f0f5024..f3e6a0dc71edecd6c6ef525a3f0189a9d652b829 100644
--- a/opam
+++ b/opam
@@ -119,7 +119,7 @@ run-test: [
]
depends: [
- "dune" { >= "3.2.0" | (>= "3.5.0" & os="macos") }
+ "dune" { >= "3.3.0" | (>= "3.5.0" & os="macos") }
"dune-configurator"
"dune-site"
diff --git a/src/kernel_services/abstract_interp/abstract_interp.mli b/src/kernel_services/abstract_interp/abstract_interp.mli
index c2c809122d2058859a8f14bf28e6e114bfe1de90..bcc9ed9915bfa80e78859a968f02fe3578a49523 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.mli
+++ b/src/kernel_services/abstract_interp/abstract_interp.mli
@@ -118,7 +118,7 @@ module type Collapse = sig val collapse : bool end
(** If [C.collapse] then [L1.bottom,_] = [_,L2.bottom] = [bottom] *)
(* Untested *)
-module Make_Lattice_Product (L1:AI_Lattice_with_cardinal_one) (L2:AI_Lattice_with_cardinal_one) (C:Collapse):
+module Make_Lattice_Product (L1:AI_Lattice_with_cardinal_one) (L2:AI_Lattice_with_cardinal_one) (_:Collapse):
Lattice_Product with type t1 = L1.t and type t2 = L2.t
(** Uncollapsed product. Literally the set of (e1, e2) ordered pairs
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 2b584a1a1d28f8f3331bd0325152a951a5a6e97f..5717cc78c7bfb6b68537bb40f4533e52e7101cdd 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -32,6 +32,16 @@ type 'a default_contents =
| Constant of 'a
| Other
+
+module type Default_offsetmap = sig
+ type v
+ type offsetmap
+
+ val name: string
+ val default_offsetmap : Base.t -> offsetmap Lattice_bounds.or_bottom
+ val default_contents: v default_contents
+end
+
module Make_LOffset
(V: sig
include Offsetmap_lattice_with_isotropy.S
@@ -40,11 +50,8 @@ module Make_LOffset
(Offsetmap: Offsetmap_sig.S
with type v = V.t
and type widen_hint = V.numerical_widen_hint)
- (Default_offsetmap: sig
- val name: string
- val default_offsetmap : Base.t -> Offsetmap.t or_bottom
- val default_contents: V.t default_contents
- end)
+ (Default_offsetmap: Default_offsetmap with type v := V.t
+ and type offsetmap := Offsetmap.t)
=
struct
diff --git a/src/kernel_services/abstract_interp/lmap.mli b/src/kernel_services/abstract_interp/lmap.mli
index bf5710f72eef96ef60c7458e28e8acd2937b9a87..b7bfddf3611be3b582087c74b25e0abcb1a05cdb 100644
--- a/src/kernel_services/abstract_interp/lmap.mli
+++ b/src/kernel_services/abstract_interp/lmap.mli
@@ -25,51 +25,56 @@
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
(** Contents of a variable when it is not present in the state.
- See function [default_contents] in the functor below *)
+ See function [default_contents] in the signature below *)
type 'a default_contents =
| Bottom
| Top of 'a
| Constant of 'a
| Other
+module type Default_offsetmap = sig
+ type v
+ type offsetmap
+
+ val name: string
+ (** Used to create different datatypes each time the functor is applied *)
+
+ val default_offsetmap : Base.t -> offsetmap Lattice_bounds.or_bottom
+ (** Value returned when a map is queried, and the base is not present.
+ [`Bottom] indicates that the base is never bound in such a map. *)
+
+ val default_contents: v default_contents
+ (** This function is used to optimize functions that add keys in a map,
+ in particular when maintaining canonicity w.r.t. default contents.
+ It describes the contents [c] of the offsetmap
+ resulting from [default_offsetmap b]. The possible values are:
+ - [Bottom] means that [c] is [V.bottom] everywhere, and furthermore
+ that [V.bottom] has an empty concretization. We deduce from this
+ fact that unmapped keys do not contribute to a join, and that
+ [join c v] is never [c] as soon as [v] is not itself [v].
+ - [Top] means that [c] is [V.top] everywhere. Thus unmapped keys
+ have a default value more general than the one in a map where the
+ key is bound.
+ - [`Constant v] means that [c] is an offsetmap with a single interval
+ containing [v] everywhere. [v] must be isotropic (in the sense
+ of {!V.is_isotropic}).
+ - [`Other] means that [default_offsetmap] returns something arbitrary.
+
+ This function is only used on keys that change values. Thus it is
+ safe to have [default_offsetmap] return something that do not
+ match [default_contents] on constant keys.
+ *)
+end
+
module Make_LOffset
(V: sig
include Offsetmap_lattice_with_isotropy.S
include Lattice_type.With_Top_Opt with type t := t
end)
- (Offsetmap: Offsetmap_sig.S
- with type v = V.t
- and type widen_hint = V.numerical_widen_hint)
- (Default_offsetmap: sig
- val name: string
- (** Used to create different datatypes each time the functor is applied *)
-
- val default_offsetmap : Base.t -> Offsetmap.t Lattice_bounds.or_bottom
- (** Value returned when a map is queried, and the base is not present.
- [`Bottom] indicates that the base is never bound in such a map. *)
-
- val default_contents: V.t default_contents
- (** This function is used to optimize functions that add keys in a map,
- in particular when maintaining canonicity w.r.t. default contents.
- It describes the contents [c] of the offsetmap
- resulting from [default_offsetmap b]. The possible values are:
- - [Bottom] means that [c] is [V.bottom] everywhere, and furthermore
- that [V.bottom] has an empty concretization. We deduce from this
- fact that unmapped keys do not contribute to a join, and that
- [join c v] is never [c] as soon as [v] is not itself [v].
- - [Top] means that [c] is [V.top] everywhere. Thus unmapped keys
- have a default value more general than the one in a map where the
- key is bound.
- - [`Constant v] means that [c] is an offsetmap with a single interval
- containing [v] everywhere. [v] must be isotropic (in the sense
- of {!V.is_isotropic}).
- - [`Other] means that [default_offsetmap] returns something arbitrary.
-
- This function is only used on keys that change values. Thus it is
- safe to have [default_offsetmap] return something that do not
- match [default_contents] on constant keys.
- *)
- end):
+ (Offsetmap: Offsetmap_sig.S with type v = V.t
+ and type widen_hint = V.numerical_widen_hint)
+ (_: Default_offsetmap with type v := V.t
+ and type offsetmap := Offsetmap.t):
Lmap_sig.S
with type v = V.t
and type widen_hint_base = V.numerical_widen_hint
diff --git a/src/kernel_services/abstract_interp/lmap_sig.ml b/src/kernel_services/abstract_interp/lmap_sig.ml
index d901a9cf110d08c59a7affde179a38ede87d81cd..37839ffd1a34d994a3d7d70bb5953e27aca0c599 100644
--- a/src/kernel_services/abstract_interp/lmap_sig.ml
+++ b/src/kernel_services/abstract_interp/lmap_sig.ml
@@ -73,7 +73,7 @@ module type S = sig
val join : t -> t -> t
val is_included : t -> t -> bool
- module Make_Narrow(X: sig
+ module Make_Narrow(_: sig
include Lattice_type.With_Top with type t := v
include Lattice_type.With_Narrow with type t := v
val bottom_is_strict: bool
diff --git a/src/kernel_services/abstract_interp/map_lattice.mli b/src/kernel_services/abstract_interp/map_lattice.mli
index 07224c875db63932871bbb9992f47bb11ddee6c6..baed8f769c4bb80eceb05f8048989b2bc586a577 100644
--- a/src/kernel_services/abstract_interp/map_lattice.mli
+++ b/src/kernel_services/abstract_interp/map_lattice.mli
@@ -172,8 +172,8 @@ module Make_Map_Lattice
keys, indicating whether a key represents a summary of possibly multiple
keys; a binding to such a key has never a cardinality of one. *)
module With_Cardinality
- (K: sig val is_summary: Key.t -> bool end)
- (Value :
+ (_: sig val is_summary: Key.t -> bool end)
+ (_:
Lattice_type.Full_AI_Lattice_with_cardinality with type t := Value.t)
: Map_Lattice_with_cardinality with type t := t
and type key := key
@@ -198,9 +198,9 @@ module Make_MapSet_Lattice
and type v := Value.t
module With_Cardinality
- (KVMap : Map_Lattice_with_cardinality with type t := KVMap.t
- and type key := Key.t
- and type v := Value.t)
+ (_ : Map_Lattice_with_cardinality with type t := KVMap.t
+ and type key := Key.t
+ and type v := Value.t)
: MapSet_Lattice_with_cardinality with type t := t
and type key := Key.t
and type v := Value.t
diff --git a/src/kernel_services/abstract_interp/offsetmap_sig.ml b/src/kernel_services/abstract_interp/offsetmap_sig.ml
index e1aff75607b0f7998b6cdb21eb850cdbeb4f01de..70834f81755f713f1cd083b5d226720fd8829499 100644
--- a/src/kernel_services/abstract_interp/offsetmap_sig.ml
+++ b/src/kernel_services/abstract_interp/offsetmap_sig.ml
@@ -160,7 +160,7 @@ module type S = sig
(** {2 Narrowing} *)
- module Make_Narrow (X: sig
+ module Make_Narrow (_: sig
include Lattice_type.With_Top with type t := v
include Lattice_type.With_Narrow with type t := v
end) : sig
diff --git a/src/kernel_services/analysis/dataflow2.mli b/src/kernel_services/analysis/dataflow2.mli
index b74e55b8604e8502af361d7065ece648dcc2b142..c8bada2cdbd0e66193f431d9720d129a2917febc 100644
--- a/src/kernel_services/analysis/dataflow2.mli
+++ b/src/kernel_services/analysis/dataflow2.mli
@@ -135,7 +135,7 @@ module type ForwardsTransfer = sig
end
-module Forwards(T : ForwardsTransfer) : sig
+module Forwards(_ : ForwardsTransfer) : sig
val compute: Cil_types.stmt list -> unit
(** Fill in the T.stmtStartData, given a number of initial statements to
start from. All of the initial statements must have some entry in
@@ -210,7 +210,7 @@ module type BackwardsTransfer = sig
end
-module Backwards(T : BackwardsTransfer) : sig
+module Backwards(_ : BackwardsTransfer) : sig
val compute: Cil_types.stmt list -> unit
(** Fill in the T.stmtStartData, given a number of initial statements to start
from (the sinks for the backwards data flow). All of the statements (not
diff --git a/src/kernel_services/analysis/dataflows.mli b/src/kernel_services/analysis/dataflows.mli
index e96672e84c2ab130a76ecbe36fe043a3659bdd94..438d16c03b7edb9bd75d39b7d9995cdb4e434c31 100644
--- a/src/kernel_services/analysis/dataflows.mli
+++ b/src/kernel_services/analysis/dataflows.mli
@@ -118,7 +118,7 @@ module type BACKWARD_MONOTONE_PARAMETER = sig
val init: (stmt * t) list
end
-module Simple_backward(Fenv:FUNCTION_ENV)(P:BACKWARD_MONOTONE_PARAMETER) : sig
+module Simple_backward(_:FUNCTION_ENV)(P:BACKWARD_MONOTONE_PARAMETER) : sig
(** {3 Retrieving the state before and after a statement.} *)
@@ -177,7 +177,7 @@ module type FORWARD_MONOTONE_PARAMETER = sig
end
-module Simple_forward(Fenv:FUNCTION_ENV)(P:FORWARD_MONOTONE_PARAMETER) : sig
+module Simple_forward(_:FUNCTION_ENV)(P:FORWARD_MONOTONE_PARAMETER) : sig
(** {3 Retrieve the state before and after a statement.} *)
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index ef8d9447bb247dbed4a547211dd71642c473714c..49a00d082eeaacd16b101bd03bbfe85c593a3626 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -293,7 +293,7 @@ val get_called : exp -> t option
(** Hashtable indexed by kernel functions and dealing with project.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-module Make_Table(Data: Datatype.S)(Info: State_builder.Info_with_size):
+module Make_Table(Data: Datatype.S)(_: State_builder.Info_with_size):
State_builder.Hashtbl with type key = t and type data = Data.t
(** Set of kernel functions. *)
diff --git a/src/kernel_services/ast_printing/printer_api.ml b/src/kernel_services/ast_printing/printer_api.ml
index 3dabf90e2ddf04f36261001d804ca8500d777284..4578370ef0676406c3f86afeaa5566a5cce6631f 100644
--- a/src/kernel_services/ast_printing/printer_api.ml
+++ b/src/kernel_services/ast_printing/printer_api.ml
@@ -532,7 +532,7 @@ module type S = sig
(** Signature for extending an existing pretty-printer. OCaml forbids
inheriting from a class received as argument, so we use a functor
instead. *)
- module type PrinterExtension = functor (X: PrinterClass) -> PrinterClass
+ module type PrinterExtension = functor (_: PrinterClass) -> PrinterClass
val update_printer: (module PrinterExtension) -> unit
(** Register a pretty-printer extension. The pretty-printer passed as
diff --git a/src/kernel_services/ast_printing/printer_builder.ml b/src/kernel_services/ast_printing/printer_builder.ml
index 7eca5d41378ab011942043c7d16e9c64f590a700..7a2dda14c7cfc896bd9334f0a69d4645338eaafc 100644
--- a/src/kernel_services/ast_printing/printer_builder.ml
+++ b/src/kernel_services/ast_printing/printer_builder.ml
@@ -111,7 +111,7 @@ struct
let printer_ref = ref None
- module type PrinterExtension = functor (X: PrinterClass) -> PrinterClass
+ module type PrinterExtension = functor (_: PrinterClass) -> PrinterClass
let set_printer p =
printer_class_ref := p;
diff --git a/src/kernel_services/ast_printing/printer_builder.mli b/src/kernel_services/ast_printing/printer_builder.mli
index 7310b8d3adcfcdbddaa939ddd748ec2a2f445b60..9a817d00604b8e118cef89907d486b992f54e64d 100644
--- a/src/kernel_services/ast_printing/printer_builder.mli
+++ b/src/kernel_services/ast_printing/printer_builder.mli
@@ -24,14 +24,14 @@
object obtained by (P()) *)
module Make_pp
- (P: sig val printer: unit -> Printer_api.extensible_printer_type end):
+ (_: sig val printer: unit -> Printer_api.extensible_printer_type end):
Printer_api.S_pp
(** Build a full pretty-printer from a pretty-printing class.
@since Fluorine-20130401 *)
module Make
- (P: sig class printer: unit -> Printer_api.extensible_printer_type end):
+ (_: sig class printer: unit -> Printer_api.extensible_printer_type end):
Printer_api.S
(*
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
index 741b922ff24653872f973426b4214070076868d2..0171b029d99e97ec18301802b904461a4473181e 100644
--- a/src/kernel_services/ast_printing/printer_tag.mli
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -90,6 +90,6 @@ sig
(Format.formatter -> 'a -> unit)
end
-module Make(T : Tag) : S_pp
+module Make(_ : Tag) : S_pp
(* -------------------------------------------------------------------------- *)
diff --git a/src/kernel_services/ast_queries/cil_state_builder.mli b/src/kernel_services/ast_queries/cil_state_builder.mli
index 0c61506c8625b86c904e5c4f5a3cd82e73e8b802..cafc3bdc85d74ced6be8f68cae7ab53cab21d5f0 100644
--- a/src/kernel_services/ast_queries/cil_state_builder.mli
+++ b/src/kernel_services/ast_queries/cil_state_builder.mli
@@ -23,30 +23,30 @@
(** Functors for building computations which use kernel datatypes.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-module Stmt_set_ref(Info: State_builder.Info) :
+module Stmt_set_ref(_: State_builder.Info) :
State_builder.Set_ref with type elt = Cil_types.stmt
-module Kinstr_hashtbl(Data:Datatype.S)(Info: State_builder.Info_with_size) :
+module Kinstr_hashtbl(Data:Datatype.S)(_: State_builder.Info_with_size) :
State_builder.Hashtbl with type key = Cil_types.kinstr and type data = Data.t
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-module Stmt_hashtbl(Data:Datatype.S)(Info: State_builder.Info_with_size) :
+module Stmt_hashtbl(Data:Datatype.S)(_: State_builder.Info_with_size) :
State_builder.Hashtbl with type key = Cil_types.stmt and type data = Data.t
-module Varinfo_hashtbl(Data:Datatype.S)(Info: State_builder.Info_with_size) :
+module Varinfo_hashtbl(Data:Datatype.S)(_: State_builder.Info_with_size) :
State_builder.Hashtbl with type key = Cil_types.varinfo
and type data = Data.t
-module Exp_hashtbl(Data:Datatype.S)(Info: State_builder.Info_with_size) :
+module Exp_hashtbl(Data:Datatype.S)(_: State_builder.Info_with_size) :
State_builder.Hashtbl with type key = Cil_types.exp
and type data = Data.t
-module Lval_hashtbl(Data:Datatype.S)(Info: State_builder.Info_with_size) :
+module Lval_hashtbl(Data:Datatype.S)(_: State_builder.Info_with_size) :
State_builder.Hashtbl with type key = Cil_types.lval
and type data = Data.t
module Kernel_function_hashtbl
- (Data:Datatype.S)(Info: State_builder.Info_with_size):
+ (Data:Datatype.S)(_: State_builder.Info_with_size):
State_builder.Hashtbl with type key = Cil_types.kernel_function
and type data = Data.t
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index f9f671cb80244851652504b355a6e099fe1e218a..9f4653e1d6d5e5c3696a2281c50cad012df28d2d 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -219,7 +219,7 @@ sig
end
module Make
- (C :
+ (_ :
sig
val is_loop: unit -> bool
(** whether the annotation we want to type is contained in a loop.
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.mli b/src/kernel_services/cmdline_parameters/parameter_builder.mli
index eb5e2c968f0b30131e7cd5d63d5bac965760f04b..7e0e933bd266ff2adeaf3711c9c59193cbab88ef 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.mli
@@ -27,7 +27,7 @@
(* ************************************************************************* *)
module Make
- (P: sig
+ (_: sig
val shortname: string
val parameters: (string, Typed_parameter.t list) Hashtbl.t
module L: sig
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.ml b/src/kernel_services/cmdline_parameters/parameter_sig.ml
index 31d72fe5961b6a2ffcfe45da400988435056e824..7b27f9a778ae3bd009c9034277491e780aabe6f3 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.ml
@@ -523,34 +523,34 @@ module type Builder = sig
@since Sodium-20150201
*)
- module Bool(X:sig include Input val default: bool end): Bool
- module Action(X: Input) : Bool
+ module Bool(_:sig include Input val default: bool end): Bool
+ module Action(_: Input) : Bool
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- module False(X: Input) : Bool
+ module False(_: Input) : Bool
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- module True(X: Input) : Bool
+ module True(_: Input) : Bool
module WithOutput
- (X: sig include Input val output_by_default: bool end):
+ (_: sig include Input val output_by_default: bool end):
With_output
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- module Int(X: sig include Input_with_arg val default: int end): Int
+ module Int(_: sig include Input_with_arg val default: int end): Int
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- module Zero(X: Input_with_arg): Int
+ module Zero(_: Input_with_arg): Int
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- module String(X: sig include Input_with_arg val default: string end): String
+ module String(_: sig include Input_with_arg val default: string end): String
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- module Empty_string(X: Input_with_arg): String
+ module Empty_string(_: Input_with_arg): String
module Fc_Filepath = Filepath
- module Filepath(X: sig
+ module Filepath(_: sig
include Input_with_arg
val existence: Filepath.existence
val file_kind: string
@@ -565,21 +565,21 @@ module type Builder = sig
include String_datatype_with_collections
val of_singleton_string: string -> Set.t
end)
- (X: sig include Input_collection val default: E.Set.t end):
+ (_: sig include Input_collection val default: E.Set.t end):
Set with type elt = E.t and type t = E.Set.t
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- module String_set(X: Input_with_arg): String_set
+ module String_set(_: Input_with_arg): String_set
module Filled_string_set
- (X: sig
+ (_: sig
include Input_with_arg
val default: Datatype.String.Set.t
end): String_set
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- module Kernel_function_set(X: Input_with_arg): Kernel_function_set
- module Fundec_set(X: Input_with_arg): Fundec_set
+ module Kernel_function_set(_: Input_with_arg): Kernel_function_set
+ module Fundec_set(_: Input_with_arg): Fundec_set
module Make_list
(E:
@@ -587,13 +587,13 @@ module type Builder = sig
include String_datatype
val of_singleton_string: string -> t list
end)
- (X: sig include Input_collection val default: E.t list end):
+ (_: sig include Input_collection val default: E.t list end):
List with type elt = E.t and type t = E.t list
- module String_list(X: Input_with_arg): String_list
+ module String_list(_: Input_with_arg): String_list
module Filepath_list
- (X: sig
+ (_: sig
include Input_with_arg
val existence: Fc_Filepath.existence
val file_kind: string
@@ -602,7 +602,7 @@ module type Builder = sig
module Filepath_map
(V: Value_datatype with type key = Fc_Filepath.Normalized.t)
- (X: sig
+ (_: sig
include Input_with_arg
val default: V.t Datatype.Filepath.Map.t
val existence: Fc_Filepath.existence
@@ -617,13 +617,13 @@ module type Builder = sig
module Make_map
(K: String_datatype_with_collections)
(V: Value_datatype with type key = K.t)
- (X: sig include Input_collection val default: V.t K.Map.t end):
+ (_: sig include Input_collection val default: V.t K.Map.t end):
Map
with type key = K.t and type value = V.t and type t = V.t K.Map.t
module String_map
(V: Value_datatype with type key = string)
- (X: sig include Input_with_arg val default: V.t Datatype.String.Map.t end):
+ (_: sig include Input_with_arg val default: V.t Datatype.String.Map.t end):
Map
with type key = string
and type value = V.t
@@ -634,7 +634,7 @@ module type Builder = sig
pure prototypes. *)
module Kernel_function_map
(V: Value_datatype with type key = Cil_types.kernel_function)
- (X: sig include Input_with_arg val default: V.t Cil_datatype.Kf.Map.t end):
+ (_: sig include Input_with_arg val default: V.t Cil_datatype.Kf.Map.t end):
Map
with type key = Cil_types.kernel_function
and type value = V.t
@@ -644,13 +644,13 @@ module type Builder = sig
module Make_multiple_map
(K: String_datatype_with_collections)
(V: Multiple_value_datatype with type key = K.t)
- (X: sig include Input_collection val default: V.t list K.Map.t end):
+ (_: sig include Input_collection val default: V.t list K.Map.t end):
Multiple_map
with type key = K.t and type value = V.t and type t = V.t list K.Map.t
module String_multiple_map
(V: Multiple_value_datatype with type key = string)
- (X: sig
+ (_: sig
include Input_with_arg
val default: V.t list Datatype.String.Map.t
end):
@@ -664,7 +664,7 @@ module type Builder = sig
pure prototypes. *)
module Kernel_function_multiple_map
(V: Multiple_value_datatype with type key = Cil_types.kernel_function)
- (X: sig
+ (_: sig
include Input_with_arg
val default: V.t list Cil_datatype.Kf.Map.t
end):
diff --git a/src/kernel_services/cmdline_parameters/parameter_state.mli b/src/kernel_services/cmdline_parameters/parameter_state.mli
index f4bdcfa8effbd6e4d3e51aa6232cfd6184e7d642..fd87b9deeb9ee27b7d05cf1cd63bd10d18d88a50 100644
--- a/src/kernel_services/cmdline_parameters/parameter_state.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_state.mli
@@ -47,7 +47,7 @@ val get_reset_selection: ?is_set:bool -> unit -> State_selection.t
(* ************************************************************************* *)
module Make
- (P: sig val shortname: string end)
+ (_: sig val shortname: string end)
(X:sig
include Datatype.S
val default: unit -> t
diff --git a/src/kernel_services/plugin_entry_points/emitter.mli b/src/kernel_services/plugin_entry_points/emitter.mli
index 6215281eb6f1e14ce0421fad747cb59d70e90352..afe5b5767f6be59dc801b927a3e74bd9cbb42e38 100644
--- a/src/kernel_services/plugin_entry_points/emitter.mli
+++ b/src/kernel_services/plugin_entry_points/emitter.mli
@@ -127,7 +127,7 @@ module Make_table
val get: t -> emitter
end)
(D: Datatype.S)
- (Info: sig include State_builder.Info_with_size val kinds: kind list end) :
+ (_: sig include State_builder.Info_with_size val kinds: kind list end) :
sig
type internal_tbl = D.t E.Hashtbl.t
val self: State.t
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index fec09bc71b5a023d9db139d8250e1519c2d1e772..624898fa1cb79edb552ebbe18fe63cee83364615 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -228,7 +228,7 @@ module type Input_with_arg = sig
val module_name: string
end
-module Kernel_function_set(X:Input_with_arg): Parameter_sig.Kernel_function_set
+module Kernel_function_set(_:Input_with_arg): Parameter_sig.Kernel_function_set
(* ************************************************************************* *)
(** {2 Option groups} *)
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index a3c6d693e3fb2e1cde6c22759c09456705e8e11f..2f006e98e40d9f376f675f4b1c9c988fa69367f8 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -380,7 +380,7 @@ val is_subcategory : string list -> string list -> bool
They should apply {!Plugin.Register} instead.
@since Beryllium-20090601-beta1 *)
module Register
- (P : sig
+ (_ : sig
val channel : string
val label : string
val verbose_atleast : int -> bool
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 75c75aa1ae7280d74a2a527901db0140dbe70307..cf1aac9575fb466a1444ff4f0f001511e300c29a 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -109,7 +109,7 @@ val register_kernel: unit -> unit
services.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Register
- (P: sig
+ (_: sig
val name: string
(** Name of the module. Arbitrary non-empty string. *)
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 39e4baadec51035688238e414ffa8fe726f99f87..54bbb2ec476ef53f16a3e008e02b01c9b387169d 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -290,7 +290,7 @@ module Make_with_collections(X: Make_input):
(** Add sets, maps and hashtables modules to an existing datatype, provided the
[equal], [compare] and [hash] functions are not {!undefined}.
@since Oxygen-20120901 *)
-module With_collections(X: S)(Info: Functor_info):
+module With_collections(X: S)(_: Functor_info):
S_with_collections with type t = X.t
(* ****************************************************************************)
@@ -508,7 +508,7 @@ module Poly_pair: Polymorphic2 with type ('a, 'b) poly = 'a * 'b
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Pair(T1: S)(T2: S): S with type t = T1.t * T2.t
-module Pair_with_collections(T1: S)(T2: S)(Info: Functor_info):
+module Pair_with_collections(T1: S)(T2: S)(_: Functor_info):
S_with_collections with type t = T1.t * T2.t
val pair: 'a Type.t -> 'b Type.t -> ('a * 'b) Type.t
@@ -522,7 +522,7 @@ module Poly_option: Polymorphic with type 'a poly = 'a option
module Option(T: S) : S with type t = T.t option
(** @since Nitrogen-20111001 *)
-module Option_with_collections(T:S)(Info: Functor_info):
+module Option_with_collections(T:S)(_: Functor_info):
S_with_collections with type t = T.t option
val option: 'a Type.t -> 'a option Type.t
@@ -532,7 +532,7 @@ module Poly_list: Polymorphic with type 'a poly = 'a list
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module List(T: S) : S with type t = T.t list
-module List_with_collections(T:S)(Info:Functor_info):
+module List_with_collections(T:S)(_:Functor_info):
S_with_collections with type t = T.t list
(** @since Fluorine-20130401 *)
@@ -545,7 +545,7 @@ module Poly_array: Polymorphic with type 'a poly = 'a array
module Array(T: S) : S with type t = T.t array
(** @since Neon-20140301 *)
-module Array_with_collections(T:S)(Info:Functor_info):
+module Array_with_collections(T:S)(_:Functor_info):
S_with_collections with type t = T.t array
(** @since Neon-20140301 *)
@@ -561,7 +561,7 @@ module Triple(T1: S)(T2: S)(T3: S): S with type t = T1.t * T2.t * T3.t
val triple: 'a Type.t -> 'b Type.t -> 'c Type.t -> ('a * 'b * 'c) Type.t
(** @since Fluorine-20130401 *)
-module Triple_with_collections(T1: S)(T2: S)(T3: S)(Info: Functor_info):
+module Triple_with_collections(T1: S)(T2: S)(T3: S)(_: Functor_info):
S_with_collections with type t = T1.t * T2.t * T3.t
(** @since Nitrogen-20111001 *)
@@ -573,7 +573,7 @@ val quadruple:
(** @since Nitrogen-20111001 *)
module Quadruple_with_collections
- (T1: S)(T2: S)(T3: S)(T4:S)(Info: Functor_info):
+ (T1: S)(T2: S)(T3: S)(T4:S)(_: Functor_info):
S_with_collections with type t = T1.t * T2.t * T3.t * T4.t
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
@@ -617,15 +617,15 @@ val func4:
('a -> 'b -> 'c -> 'd -> 'e) Type.t
module Set
- (S: Set.S)(E: S with type t = S.elt)(Info : Functor_info):
+ (S: Set.S)(E: S with type t = S.elt)(_ : Functor_info):
Set with type t = S.t and type elt = E.t
module Map
- (M: Map.S)(Key: S with type t = M.key)(Info: Functor_info) :
+ (M: Map.S)(Key: S with type t = M.key)(_: Functor_info) :
Map with type 'a t = 'a M.t and type key = M.key and module Key = Key
module Hashtbl
- (H: Hashtbl_with_descr)(Key: S with type t = H.key)(Info : Functor_info):
+ (H: Hashtbl_with_descr)(Key: S with type t = H.key)(_: Functor_info):
Hashtbl with type 'a t = 'a H.t and type key = H.key and module Key = Key
module type Sub_caml_weak_hashtbl = sig
@@ -640,7 +640,7 @@ module Caml_weak_hashtbl(D: S): sig
module Datatype: S with type t = t
end
-module Weak(W: Sub_caml_weak_hashtbl)(D: S with type t = W.data) :
+module Weak(W: Sub_caml_weak_hashtbl)(_: S with type t = W.data) :
S with type t = W.t
(*
diff --git a/src/libraries/datatype/type.mli b/src/libraries/datatype/type.mli
index 554739c80b57e1b5add9b38082468497b335ab47..18b02aa6d97f1ecf1aa34b2a5af3606bd71d6a8d 100644
--- a/src/libraries/datatype/type.mli
+++ b/src/libraries/datatype/type.mli
@@ -108,7 +108,7 @@ exception No_abstract_type of string
@raise No_abstract_type if no such abstract type was registered.
@since Nitrogen-20111001
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-module Abstract(T: sig val name: string end): sig
+module Abstract(_: sig val name: string end): sig
type t
val ty: t ty
end
diff --git a/src/libraries/project/project_skeleton.mli b/src/libraries/project/project_skeleton.mli
index ddd012828a1426f512bd072a6d213ca0ee23629a..0203ec3fb007e654a66c2c543af63e666e284221 100644
--- a/src/libraries/project/project_skeleton.mli
+++ b/src/libraries/project/project_skeleton.mli
@@ -54,7 +54,7 @@ val dummy: t
(** @since Carbon-20101201 *)
(** @since Carbon-20101201 *)
-module Make_setter(X: sig val mem: string -> bool end) : sig
+module Make_setter(_: sig val mem: string -> bool end) : sig
val make_unique_name: string -> string
(** @return a fresh name from the given string according to [X.mem].
diff --git a/src/libraries/project/state_builder.ml b/src/libraries/project/state_builder.ml
index a65f82560e349fd7979a1cba0a505e44f2ec960a..ec3da06c000d094118f4b4366bca117e388c2d45 100644
--- a/src/libraries/project/state_builder.ml
+++ b/src/libraries/project/state_builder.ml
@@ -801,7 +801,7 @@ module type Hashconsing_tbl =
val hash_internal: t -> int
val initial_values: t list
end) ->
- functor (Info: Info_with_size) ->
+ functor (_: Info_with_size) ->
Weak_hashtbl with type data = Data.t
module Hashconsing_tbl =
diff --git a/src/libraries/project/state_builder.mli b/src/libraries/project/state_builder.mli
index edf54150e1d077b84a7fccddf386d7962946301a..e3abcf1f38a5b81abb9142bba7a888265fd8c3be 100644
--- a/src/libraries/project/state_builder.mli
+++ b/src/libraries/project/state_builder.mli
@@ -81,15 +81,15 @@ module type S = sig
end
-(** [Register(Datatype)(State)(Info)] registers a new state.
+(** [Register(Datatype)(Local_state)(Info)] registers a new state.
[Datatype] represents the datatype of a state, [Local_state]
explains how to deal with the client-side state and [Info] are additional
required information.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Register
(Datatype: Datatype.S)
- (Local_state: State.Local with type t = Datatype.t)
- (Info: sig include Info val unique_name: string end)
+ (_: State.Local with type t = Datatype.t)
+ (_: sig include Info val unique_name: string end)
: S with module Datatype = Datatype
(* ************************************************************************* *)
@@ -127,7 +127,7 @@ end
(** @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
module Ref
(Data:Datatype.S)
- (Info:sig
+ (_:sig
include Info
val default: unit -> Data.t
end)
@@ -156,7 +156,7 @@ module type Option_ref = sig
end
(** Build a reference on an option. *)
-module Option_ref(Data:Datatype.S)(Info: Info) :
+module Option_ref(Data:Datatype.S)(_: Info) :
Option_ref with type data = Data.t
(** Output signature of [ListRef].
@@ -173,34 +173,34 @@ end
(** Build a reference on a list.
@since Boron-20100401 *)
-module List_ref(Data:Datatype.S)(Info: Info) :
+module List_ref(Data:Datatype.S)(_: Info) :
List_ref with type data = Data.t list and type data_in_list = Data.t
(** Build a reference on an integer.
@since Carbon-20101201 *)
-module Int_ref(Info:sig include Info val default: unit -> int end) :
+module Int_ref(_:sig include Info val default: unit -> int end) :
Ref with type data = int
(** Build a reference on an integer, initialized with [0].
@since Carbon-20101201 *)
-module Zero_ref(Info:Info) : Ref with type data = int
+module Zero_ref(_:Info) : Ref with type data = int
(** Build a reference on a boolean.
@since Oxygen-20120901 *)
-module Bool_ref(Info:sig include Info val default: unit -> bool end) :
+module Bool_ref(_:sig include Info val default: unit -> bool end) :
Ref with type data = bool
(** Build a reference on a boolean, initialized with [false].
@since Carbon-20101201 *)
-module False_ref(Info:Info): Ref with type data = bool
+module False_ref(_:Info): Ref with type data = bool
(** Build a reference on a boolean, initialized with [true].
@since Carbon-20101201 *)
-module True_ref(Info:Info): Ref with type data = bool
+module True_ref(_:Info): Ref with type data = bool
(** Build a reference on a float.
@since Oxygen-20120901 *)
-module Float_ref(Info:sig include Info val default: unit -> float end) :
+module Float_ref(_:sig include Info val default: unit -> float end) :
Ref with type data = float
(* ************************************************************************* *)
@@ -269,13 +269,13 @@ end
[W].
@since Boron-20100401 *)
module Weak_hashtbl
- (W: Weak.S)(Data: Datatype.S with type t = W.data)(Info: Info_with_size) :
+ (W: Weak.S)(_: Datatype.S with type t = W.data)(_: Info_with_size) :
Weak_hashtbl with type data = W.data
(** Build a weak hashtbl over a datatype [Data] by using [Weak.Make] provided
by the OCaml standard library. Note that the table is not saved on disk.
@since Boron-20100401 *)
-module Caml_weak_hashtbl(Data: Datatype.S)(Info: Info_with_size) :
+module Caml_weak_hashtbl(Data: Datatype.S)(_: Info_with_size) :
Weak_hashtbl with type data = Data.t
(** Signature for the creation of projectified hashconsing tables..
@@ -296,7 +296,7 @@ module type Hashconsing_tbl =
(** Pre-existing values stored in the built table and shared by all
existing projects. *)
end) ->
- functor (Info: Info_with_size) ->
+ functor (_: Info_with_size) ->
Weak_hashtbl with type data = Data.t
(** Weak hashtbl dedicated to hashconsing.
@@ -398,11 +398,11 @@ end
module Hashtbl
(H: Datatype.Hashtbl)
(Data: Datatype.S)
- (Info: Info_with_size) :
+ (_: Info_with_size) :
Hashtbl with type key = H.key and type data = Data.t
and module Datatype = H.Make(Data)
-module Int_hashtbl(Data: Datatype.S)(Info:Info_with_size):
+module Int_hashtbl(Data: Datatype.S)(_:Info_with_size):
Hashtbl with type key = int and type data = Data.t
(* ************************************************************************* *)
@@ -423,7 +423,7 @@ module type Set_ref = sig
val iter: (elt -> unit) -> unit
end
-module Set_ref(S: Datatype.Set)(Info: Info)
+module Set_ref(S: Datatype.Set)(_: Info)
: Set_ref with type elt = S.elt and type data = S.t
(* ************************************************************************* *)
@@ -440,7 +440,7 @@ module type Queue = sig
val length: unit -> int
end
-module Queue(Data: Datatype.S)(Info: Info) : Queue with type elt = Data.t
+module Queue(Data: Datatype.S)(_: Info) : Queue with type elt = Data.t
(* ************************************************************************* *)
(** {3 Array} *)
@@ -459,7 +459,7 @@ module type Array = sig
val fold_right: (elt -> 'a -> 'a) -> 'a -> 'a
end
-module Array(Data: Datatype.S)(Info: sig include Info val default: Data.t end) :
+module Array(Data: Datatype.S)(_: sig include Info val default: Data.t end) :
Array with type elt = Data.t
@@ -515,12 +515,12 @@ end
(** Creates a counter that is shared among all projects, but which is
marshalling-compliant.
@since Carbon-20101201 *)
-module SharedCounter(Info : sig val name : string end) : Counter
+module SharedCounter(_ : sig val name : string end) : Counter
(** Creates a projectified counter. That starts at 0
@since Nitrogen-20111001 *)
-module Counter(Info : sig val name : string end) : Counter
+module Counter(_ : sig val name : string end) : Counter
(* ****************************************************************************)
@@ -549,7 +549,7 @@ end
(** Hashconsed version of an arbitrary datatype *)
module Hashcons
(Data: Datatype.S)
- (Info: sig
+ (_: sig
include Info
val initial_values: Data.t list
(** List of values created at compile-time, that must be shared between
diff --git a/src/libraries/project/state_dependency_graph.mli b/src/libraries/project/state_dependency_graph.mli
index fa258878b836e90e9eb9a0e990f93394d14d4de9..46b9c0c99fcaf764e041925db153606e1a83bc63 100644
--- a/src/libraries/project/state_dependency_graph.mli
+++ b/src/libraries/project/state_dependency_graph.mli
@@ -71,7 +71,7 @@ include S
val add_state: State.t -> State.t list -> unit
module Attributes: Attributes
-module Dot(A: Attributes) : sig val dump: string -> unit end
+module Dot(_: Attributes) : sig val dump: string -> unit end
val dump: string -> unit
(*
diff --git a/src/libraries/qed/dune-project b/src/libraries/qed/dune-project
index 30de89263ca7599c77503f0691f5336e1f267449..d558f53e159d5b31ff821247a32f2d319265d95b 100644
--- a/src/libraries/qed/dune-project
+++ b/src/libraries/qed/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/libraries/qed/partition.mli b/src/libraries/qed/partition.mli
index 6329def9eed7e4016aec500e78a4f4cc4616e818..1f0ba435a24cae3eb1653f543a52b7d382226ab6 100644
--- a/src/libraries/qed/partition.mli
+++ b/src/libraries/qed/partition.mli
@@ -54,7 +54,7 @@ end
module Make(E : Elt)
(S : Set with type elt = E.t)
- (M : Map with type key = E.t) :
+ (_ : Map with type key = E.t) :
sig
type t
type elt = E.t
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index 04d64f4fbae2c351ec37449dbb1179535c1b3dba..462a08c1d08ea719373b93d71079834ee7c18218 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -587,16 +587,34 @@ module Shape(Key: Id_Datatype) = struct
~decide_fast ~decide_fst:decide_one ~decide_snd:decide_one ~decide_both
end
+
+module type Compositional_bool = sig
+ type key
+ type v
+
+ val e : bool
+ val f : key -> v -> bool
+ val compose : bool -> bool -> bool
+end
+
+module type Initial_values = sig
+ type key
+ type v
+ val v : (key*v) list list
+end
+
+module type Datatype_deps = sig
+ val l : State.t list
+end
+
module Make
(Key: Id_Datatype)
(V : V)
- (Compositional_bool : sig
- val e: bool
- val f : Key.t -> V.t -> bool
- val compose : bool -> bool -> bool
- end)
- (Initial_Values: sig val v : (Key.t * V.t) list list end)
- (Datatype_deps: sig val l : State.t list end)
+ (Compositional_bool : Compositional_bool with type key := Key.t
+ and type v := V.t)
+ (Initial_Values: Initial_values with type key := Key.t
+ and type v := V.t)
+ (Datatype_deps: Datatype_deps)
=
struct
diff --git a/src/libraries/utils/hptmap.mli b/src/libraries/utils/hptmap.mli
index 3f00916041af9ec45a9f6c29c8dad15bf5d49d2e..18d2595e3773499bb04b944fbbd6ab823aa7dca0 100644
--- a/src/libraries/utils/hptmap.mli
+++ b/src/libraries/utils/hptmap.mli
@@ -45,38 +45,50 @@ module Shape (Key : Id_Datatype): sig
type 'a t = 'a map
end
+(** A boolean information is maintained for each tree, by composing the
+ boolean on the subtrees and the value information present on each leaf.
+ Use {!Comp_unused} for a default implementation. *)
+module type Compositional_bool = sig
+ type key
+ type v
+
+ val e : bool
+ (** Value for the empty tree *)
+
+ val f : key -> v -> bool
+ (** Value for a leaf *)
+
+ val compose : bool -> bool -> bool
+ (** Composition of the values of two subtrees *)
+end
+
+module type Initial_values = sig
+ type key
+ type v
+ val v : (key*v) list list
+ (** List of the maps that must be shared between all instances of Frama-C
+ (the maps being described by the list of their elements).
+ Must include all maps that are exported at Caml link-time when the
+ functor is applied. This usually includes at least the empty map, hence
+ [v] nearly always contains [[]]. *)
+end
+
+module type Datatype_deps = sig
+ val l : State.t list
+ (** Dependencies of the hash-consing table. The table will be cleared
+ whenever one of those dependencies is cleared. *)
+end
+
(** This functor builds the complete module of maps indexed by keys [Key]
to values [V]. *)
module Make
(Key : Id_Datatype)
(V : V)
- (Compositional_bool : sig
- (** A boolean information is maintained for each tree, by composing the
- boolean on the subtrees and the value information present on each leaf.
- See {!Comp_unused} for a default implementation. *)
-
- val e: bool
- (** Value for the empty tree *)
-
- val f : Key.t -> V.t -> bool
- (** Value for a leaf *)
-
- val compose : bool -> bool -> bool
- (** Composition of the values of two subtrees *)
- end)
- (Initial_Values : sig
- val v : (Key.t*V.t) list list
- (** List of the maps that must be shared between all instances of Frama-C
- (the maps being described by the list of their elements).
- Must include all maps that are exported at Caml link-time when the
- functor is applied. This usually includes at least the empty map, hence
- [v] nearly always contains [[]]. *)
- end)
- (Datatype_deps: sig
- val l : State.t list
- (** Dependencies of the hash-consing table. The table will be cleared
- whenever one of those dependencies is cleared. *)
- end)
+ (_ : Compositional_bool with type key := Key.t
+ and type v := V.t)
+ (_ : Initial_values with type key := Key.t
+ and type v := V.t)
+ (_ : Datatype_deps)
: Hptmap_sig.S with type key = Key.t
and type v = V.t
and type 'v map = 'v Shape(Key).map
diff --git a/src/libraries/utils/hptset.ml b/src/libraries/utils/hptset.ml
index 7b5afc07e03b2a0fe3ed95f5418febd4ecbaec52..11c615ef411e9de8a5a69cef7071a253a1b35361 100644
--- a/src/libraries/utils/hptset.ml
+++ b/src/libraries/utils/hptset.ml
@@ -92,9 +92,18 @@ module type S = sig
val pretty_debug: t Pretty_utils.formatter
end
+module type Initial_values = sig
+ type elt
+ val v : elt list list
+end
+
+module type Datatype_deps = sig
+ val l : State.t list
+end
+
module Make(X: Hptmap.Id_Datatype)
- (Initial_Values : sig val v : X.t list list end)
- (Datatype_deps: sig val l : State.t list end) : sig
+ (Initial_values : Initial_values with type elt := X.t)
+ (Datatype_deps : Datatype_deps) : sig
include S with type elt = X.t
and type 'a map = 'a Hptmap.Shape(X).t
val self : State.t
@@ -108,7 +117,7 @@ end
(X)
(struct include Datatype.Unit let pretty_debug = pretty end)
(Hptmap.Comp_unused)
- (struct let v = List.map (List.map (fun k -> k, ())) Initial_Values.v end)
+ (struct let v = List.map (List.map (fun k -> k, ())) Initial_values.v end)
(Datatype_deps)
include M
diff --git a/src/libraries/utils/hptset.mli b/src/libraries/utils/hptset.mli
index 0adc4b3ab6332dfa419ea25227bf61c4fac1e293..afa84ebd72c521c76024dfab235b4a772da4341a 100644
--- a/src/libraries/utils/hptset.mli
+++ b/src/libraries/utils/hptset.mli
@@ -105,9 +105,25 @@ module type S = sig
val pretty_debug: t Pretty_utils.formatter
end
+module type Initial_values = sig
+ type elt
+ val v : elt list list
+ (** List of the sets that must be shared between all instances of Frama-C
+ (the sets being described by the list of their elements).
+ Must include all sets that are exported at Caml link-time when the
+ functor is applied. This usually includes at least the empty set, hence
+ [v] nearly always contains [[]]. *)
+end
+
+module type Datatype_deps = sig
+ val l : State.t list
+ (** Dependencies of the hash-consing table. The table will be cleared
+ whenever one of those dependencies is cleared. *)
+end
+
module Make(X: Hptmap.Id_Datatype)
- (Initial_Values : sig val v : X.t list list end)
- (Datatype_deps: sig val l : State.t list end) :
+ (_ : Initial_values with type elt := X.t)
+ (_ : Datatype_deps) :
sig
include S with type elt = X.t
and type 'a map = 'a Hptmap.Shape(X).map
diff --git a/src/plugins/alias/dune-project b/src/plugins/alias/dune-project
index c934d313d775e41dbb3ccc769d0dba2d1439110a..5f564c9a812ab5705915a36ed1ce66fbc4eb42bf 100644
--- a/src/plugins/alias/dune-project
+++ b/src/plugins/alias/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/aorai/dune-project b/src/plugins/aorai/dune-project
index b3c8dfe21c8184a59b18344039a80dd56cf4b275..4e033be9ebe2e1f95e6305ec09a4c16217247c6e 100644
--- a/src/plugins/aorai/dune-project
+++ b/src/plugins/aorai/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Aorai plug-in of Frama-C. ;;
diff --git a/src/plugins/api-generator/dune-project b/src/plugins/api-generator/dune-project
index 06ff92bd6eb810f0ab4547194685b2d73facb196..de387c3ced328471da2eea45a964173ff1ce03ca 100644
--- a/src/plugins/api-generator/dune-project
+++ b/src/plugins/api-generator/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/callgraph/dune-project b/src/plugins/callgraph/dune-project
index 450a812f0f250f01e0b9992cdc97b0fd064bab1d..ecc401c852c23b0140e06580da6780f4b7e23c90 100644
--- a/src/plugins/callgraph/dune-project
+++ b/src/plugins/callgraph/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/callgraph/subgraph.mli b/src/plugins/callgraph/subgraph.mli
index d294b08e06757f979b5a7ce8685cd77a7016a80c..df485369741b41eb9310737bcba5789e3336bd2f 100644
--- a/src/plugins/callgraph/subgraph.mli
+++ b/src/plugins/callgraph/subgraph.mli
@@ -28,8 +28,8 @@ module Make
val create: ?size:int -> unit -> t
val add_edge_e: t -> E.t -> unit
end)
- (D: Datatype.S with type t = G.t(* Graph datatype *))
- (Info: sig
+ (_: Datatype.S with type t = G.t(* Graph datatype *))
+ (_: sig
(** additional information *)
val self: State.t
val name: string
diff --git a/src/plugins/constant_propagation/dune-project b/src/plugins/constant_propagation/dune-project
index 7c1de9ea27de6f846ac56174c02090a169af16df..802569e45b23d55dd6aa4df9ec4941ecdb1304d9 100644
--- a/src/plugins/constant_propagation/dune-project
+++ b/src/plugins/constant_propagation/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/dive/dune-project b/src/plugins/dive/dune-project
index 09cfd9cfc031c24d89fa15891155d93e3d4b536f..a3c9521d66212c728d8229c52504db13cb6ab55f 100644
--- a/src/plugins/dive/dune-project
+++ b/src/plugins/dive/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/e-acsl/dune-project b/src/plugins/e-acsl/dune-project
index 419df63232de76a63d932b7067ac1019eca33d65..c0b8fea74abbfc1b4e27492f93e8ce99ed9852f9 100644
--- a/src/plugins/e-acsl/dune-project
+++ b/src/plugins/e-acsl/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of the Frama-C's E-ACSL plug-in. ;;
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 664c64088b858a76d9749495b6f9eea5ad9fb5fb..a48cf08b07ebba7deb21594dcd9dd4bcdb63e6c2 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -92,7 +92,7 @@ module type S = sig
end
(** Functor to build an [Error] module for a given [phase]. *)
-module Make(P: sig val phase:Options.category end): S
+module Make(_: sig val phase:Options.category end): S
(** The [Error] module implements [Error.S] with no phase. *)
include S
diff --git a/src/plugins/eva/domains/domain_builder.mli b/src/plugins/eva/domains/domain_builder.mli
index 66e384b62ac3697472b1ffb0497e3e1db135246e..2670a7e0b9e4d9a7169ff7cd8ed0dd114b61115e 100644
--- a/src/plugins/eva/domains/domain_builder.mli
+++ b/src/plugins/eva/domains/domain_builder.mli
@@ -102,6 +102,6 @@ module Complete_Simple_Cvalue
module Restrict
(Value: Abstract_value.S)
(Domain: Abstract.Domain.Internal with type value = Value.t)
- (Scope: sig val functions: Domain_mode.function_mode list end)
+ (_: sig val functions: Domain_mode.function_mode list end)
: Abstract.Domain.Internal with type value = Value.t
and type location = Domain.location
diff --git a/src/plugins/eva/domains/multidim/abstract_structure.mli b/src/plugins/eva/domains/multidim/abstract_structure.mli
index e6b28c4cfc02798d14888b3ce80234c5eafec21e..d5bd39032aff27ccb977a62ab69917dcd0483c75 100644
--- a/src/plugins/eva/domains/multidim/abstract_structure.mli
+++ b/src/plugins/eva/domains/multidim/abstract_structure.mli
@@ -49,7 +49,7 @@ sig
val map : (submemory -> submemory) -> t -> t
end
-module Make (Config : Config) (M : ProtoMemory) :
+module Make (_ : Config) (M : ProtoMemory) :
Structure with type submemory = M.t
module type Disjunction =
diff --git a/src/plugins/eva/domains/multidim/segmentation.mli b/src/plugins/eva/domains/multidim/segmentation.mli
index b2a54ee79f9d2d4e552a6d832975a3cbe7e8c9ad..2d819c5b2d891636f6fe52b955cc04e458251c28 100644
--- a/src/plugins/eva/domains/multidim/segmentation.mli
+++ b/src/plugins/eva/domains/multidim/segmentation.mli
@@ -66,5 +66,5 @@ sig
val add_segmentation_bounds : oracle:oracle -> bound list -> t -> t
end
-module Make (Config : Config) (M : ProtoMemory) :
+module Make (_ : Config) (M : ProtoMemory) :
Segmentation with type submemory = M.t
diff --git a/src/plugins/eva/domains/multidim/typed_memory.mli b/src/plugins/eva/domains/multidim/typed_memory.mli
index 530767995590b569cae6319086ae45279876dc60..bcdd9965a0d45c58ab5c3cecc5400bf78a74a57c 100644
--- a/src/plugins/eva/domains/multidim/typed_memory.mli
+++ b/src/plugins/eva/domains/multidim/typed_memory.mli
@@ -61,7 +61,7 @@ sig
val join : t -> t -> t
end
-module Make (Config : Config) (Value : Value) :
+module Make (_ : Config) (Value : Value) :
sig
type location = Abstract_offset.t
type value = Value.t
diff --git a/src/plugins/eva/domains/simple_memory.mli b/src/plugins/eva/domains/simple_memory.mli
index f1e67e165a93e697710548ad9fb8058b9a670550..0519cf24b31ba77b4fa76d2e4ca69e996474ce43 100644
--- a/src/plugins/eva/domains/simple_memory.mli
+++ b/src/plugins/eva/domains/simple_memory.mli
@@ -81,7 +81,7 @@ module type S = sig
end
(* Builds a memory from a value abstraction. *)
-module Make_Memory (Info: sig val name: string end) (Value: Value) : sig
+module Make_Memory (_: sig val name: string end) (Value: Value) : sig
include Datatype.S_with_collections
include S with type t := t
and type value := Value.t
@@ -97,7 +97,7 @@ end
(* Builds a complete Eva domain from a value abstraction. *)
module Make_Domain
- (Info: sig val name: string end)
+ (_: sig val name: string end)
(Value: Value)
: sig
diff --git a/src/plugins/eva/dune-project b/src/plugins/eva/dune-project
index 2f4a65bccf3b27de50567234e0fa2dca2f8d65d9..580cbd8f7afbabbd5fe2793b09e81c6972ffb6c3 100644
--- a/src/plugins/eva/dune-project
+++ b/src/plugins/eva/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/eva/engine/initialization.mli b/src/plugins/eva/engine/initialization.mli
index e669a8df56c486c4751b7ac4bf798c12b02af7c2..0b69e2f44ab9af5ee30106c284a2861f4042a250 100644
--- a/src/plugins/eva/engine/initialization.mli
+++ b/src/plugins/eva/engine/initialization.mli
@@ -40,9 +40,9 @@ end
module Make
(Domain: Abstract.Domain.External)
- (Eva: Evaluation_sig.S with type state = Domain.state
- and type loc = Domain.location)
- (Transfer: Transfer_stmt.S with type state = Domain.t)
+ (_: Evaluation_sig.S with type state = Domain.state
+ and type loc = Domain.location)
+ (_: Transfer_stmt.S with type state = Domain.t)
: S with type state := Domain.t
diff --git a/src/plugins/eva/engine/iterator.mli b/src/plugins/eva/engine/iterator.mli
index 4c8d02c16bbfa8a8c7d51cdf93fc0e2a719b0c57..f38056a6de251228d7952e6fa11a0857fed99ed8 100644
--- a/src/plugins/eva/engine/iterator.mli
+++ b/src/plugins/eva/engine/iterator.mli
@@ -36,14 +36,14 @@ module Computer
(* Set of states of abstract domain. *)
(States : Powerset.S with type state = Abstract.Dom.t)
(* Transfer functions for statement on the abstract domain. *)
- (Transfer : Transfer_stmt.S with type state = Abstract.Dom.t
- and type value = Abstract.Val.t)
+ (_ : Transfer_stmt.S with type state = Abstract.Dom.t
+ and type value = Abstract.Val.t)
(* Initialization of local variables. *)
- (Init: Initialization.S with type state := Abstract.Dom.t)
+ (_: Initialization.S with type state := Abstract.Dom.t)
(* Transfer functions for the logic on the abstract domain. *)
- (Logic : Transfer_logic.S with type state = Abstract.Dom.t
- and type states = States.t)
- (Spec: sig
+ (_ : Transfer_logic.S with type state = Abstract.Dom.t
+ and type states = States.t)
+ (_: sig
val treat_statement_assigns: assigns -> Abstract.Dom.t -> Abstract.Dom.t
end)
: sig
@@ -55,7 +55,6 @@ module Computer
end
-
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/eva/engine/transfer_specification.mli b/src/plugins/eva/engine/transfer_specification.mli
index 50181fb5c333ad7af5f515d26ea55c1615b9df9e..5cfd04a3e38469a4beb8ba53b0b4afd006fdc51f 100644
--- a/src/plugins/eva/engine/transfer_specification.mli
+++ b/src/plugins/eva/engine/transfer_specification.mli
@@ -26,8 +26,8 @@ open Eval
module Make
(Abstract: Abstractions.S)
(States: Powerset.S with type state = Abstract.Dom.t)
- (Logic : Transfer_logic.S with type state = Abstract.Dom.t
- and type states = States.t)
+ (_ : Transfer_logic.S with type state = Abstract.Dom.t
+ and type states = States.t)
: sig
val treat_statement_assigns: assigns -> Abstract.Dom.t -> Abstract.Dom.t
diff --git a/src/plugins/eva/partitioning/partitioning_parameters.mli b/src/plugins/eva/partitioning/partitioning_parameters.mli
index 2ecf5331712a0bdb3a1bc8dbada246a27a127891..e3243989addf804db8d30ca815e0323a74db61a1 100644
--- a/src/plugins/eva/partitioning/partitioning_parameters.mli
+++ b/src/plugins/eva/partitioning/partitioning_parameters.mli
@@ -22,7 +22,7 @@
open Cil_types
-module Make (Kf : sig val kf: kernel_function end) : sig
+module Make (_ : sig val kf: kernel_function end) : sig
val widening_delay : int
val widening_period : int
val slevel : stmt -> int
diff --git a/src/plugins/eva/partitioning/trace_partitioning.mli b/src/plugins/eva/partitioning/trace_partitioning.mli
index d6e22fb5345a33f170950df629cd0b38f6b495d1..df482f9df70eb16c7a743a53f0b6178327079dc0 100644
--- a/src/plugins/eva/partitioning/trace_partitioning.mli
+++ b/src/plugins/eva/partitioning/trace_partitioning.mli
@@ -22,7 +22,7 @@
module Make
(Abstract : Abstractions.S_with_evaluation)
- (Kf : sig val kf: Cil_types.kernel_function end) :
+ (_ : sig val kf: Cil_types.kernel_function end) :
sig
(** The states being partitioned *)
type state = Abstract.Dom.t
diff --git a/src/plugins/from/dune-project b/src/plugins/from/dune-project
index 366e01a43fef7cf345003add958bb07a52c1f142..5e5648bb0c996a09b5cc549f7ba0a04ba0d47553 100644
--- a/src/plugins/from/dune-project
+++ b/src/plugins/from/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/from/from_compute.mli b/src/plugins/from/from_compute.mli
index 1723874ad7dc4ab420dc6d628d2f1bac8eefd078..9beabb6c488608a4c1efd485a7b0d775dbff2859 100644
--- a/src/plugins/from/from_compute.mli
+++ b/src/plugins/from/from_compute.mli
@@ -57,7 +57,7 @@ val compute_using_prototype_for_state :
(** Functor computing the functional dependencies, according to the three
modules above. *)
-module Make (To_Use: To_Use) : sig
+module Make (_: To_Use) : sig
(** Compute the dependencies of the given function, and return them *)
val compute_and_return : Kernel_function.t -> Function_Froms.t
diff --git a/src/plugins/impact/dune-project b/src/plugins/impact/dune-project
index 36350966e1e87900cde5ee93dfa6c1c2aa218cd3..78ae718254d966b8e54c97042295614dfbdd9e9f 100644
--- a/src/plugins/impact/dune-project
+++ b/src/plugins/impact/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/inout/dune-project b/src/plugins/inout/dune-project
index 3319087cb684d4f3b1be17478a544c1d45a5c385..52064990516ff39f01b0fa5e3b5904813cf8d03b 100644
--- a/src/plugins/inout/dune-project
+++ b/src/plugins/inout/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/instantiate/dune-project b/src/plugins/instantiate/dune-project
index 61714be1ac1f0f6475026bb3ac7ce5c15a58242c..c166d64d9c8eddd80f43fe581e64a16dcc7643de 100644
--- a/src/plugins/instantiate/dune-project
+++ b/src/plugins/instantiate/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/instantiate/instantiator_builder.mli b/src/plugins/instantiate/instantiator_builder.mli
index 751ea0a1f5781d48bbf2b54246afffbebf6dd256..d8c77f5e02941443259ebb19ff4dbc5517978267 100644
--- a/src/plugins/instantiate/instantiator_builder.mli
+++ b/src/plugins/instantiate/instantiator_builder.mli
@@ -137,4 +137,4 @@ end
cache and function definition generation, as well as specification
registration. This should only be used by [Transform].
*)
-module Make_instantiator (G: Generator_sig) : Instantiator
+module Make_instantiator (_: Generator_sig) : Instantiator
diff --git a/src/plugins/instantiate/options.mli b/src/plugins/instantiate/options.mli
index c6f0114dcf2de7a4de6170e8e6b66a430d84fd5b..7393d7716624130bd5983c32e30e1aeb91ad5b6b 100644
--- a/src/plugins/instantiate/options.mli
+++ b/src/plugins/instantiate/options.mli
@@ -33,6 +33,6 @@ module Kfs : Parameter_sig.Kernel_function_set
to true.
*)
module NewInstantiator
- (B : sig val function_name: string end) : Parameter_sig.Bool
+ (_ : sig val function_name: string end) : Parameter_sig.Bool
val emitter: Emitter.t
diff --git a/src/plugins/instantiate/string/mem_utils.mli b/src/plugins/instantiate/string/mem_utils.mli
index ad477f5c43a13ff88e7d751ffe65a41ed304901d..c560397794d9a4625e0eb829b044209c30e9f4cf 100644
--- a/src/plugins/instantiate/string/mem_utils.mli
+++ b/src/plugins/instantiate/string/mem_utils.mli
@@ -41,7 +41,7 @@ module type Function = sig
val well_typed: typ option -> typ list -> bool
end
-module Make (F: Function) : sig
+module Make (_: Function) : sig
val generate_function_type : typ -> typ
val generate_prototype : typ -> string * typ
val well_typed_call : lval option -> varinfo -> exp list -> bool
diff --git a/src/plugins/loop_analysis/dune-project b/src/plugins/loop_analysis/dune-project
index 0db3ff404c9bbc6a9c7a096959ac492cb29f6d50..d31e06130b049620c8c7e5d0249e8d72b05f828d 100644
--- a/src/plugins/loop_analysis/dune-project
+++ b/src/plugins/loop_analysis/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/markdown-report/dune-project b/src/plugins/markdown-report/dune-project
index 5ed8ee2293837213c7731f21a0bce7f054773fa5..920d99210b4b369eef6342209f559f20150a7a3e 100644
--- a/src/plugins/markdown-report/dune-project
+++ b/src/plugins/markdown-report/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/metrics/dune-project b/src/plugins/metrics/dune-project
index 42db3b3fc021af1549c0423db5f797106b0cfb86..68310fd4976278bd416f2bdcdea69bf195b0c686 100644
--- a/src/plugins/metrics/dune-project
+++ b/src/plugins/metrics/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/nonterm/dune-project b/src/plugins/nonterm/dune-project
index 06cca356de555cfac79f0e17a7e7d9dd95f052af..df0a7bb598807478af01ce62a22602dc948fa2f1 100644
--- a/src/plugins/nonterm/dune-project
+++ b/src/plugins/nonterm/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/obfuscator/dune-project b/src/plugins/obfuscator/dune-project
index 776efcd7304909a6c7bf77656cc919d4bc0ec1dd..5ea30ad86dd693d586329ce6e7df577c77810224 100644
--- a/src/plugins/obfuscator/dune-project
+++ b/src/plugins/obfuscator/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/occurrence/dune-project b/src/plugins/occurrence/dune-project
index 0e25b9aef89901fae3f4e3ff5f92f7a7afdb821a..316594c53e43b74e2ec8febc3a65cfc54869554a 100644
--- a/src/plugins/occurrence/dune-project
+++ b/src/plugins/occurrence/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/pdg/dune-project b/src/plugins/pdg/dune-project
index 2848ef485e5fedd4ca5883d93bfee827c8ef1955..09c0389120abf233998b7f3579e035eadc5e958e 100644
--- a/src/plugins/pdg/dune-project
+++ b/src/plugins/pdg/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/postdominators/dune-project b/src/plugins/postdominators/dune-project
index 296c37ad872540185b7089c20796b156e66a71b1..20dbe0a7fa45a9a8e98aab6eba52b334a864efc5 100644
--- a/src/plugins/postdominators/dune-project
+++ b/src/plugins/postdominators/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/reduc/dune-project b/src/plugins/reduc/dune-project
index 0d005d694c5ab1c9a9f5d2f5a9013ee132297db6..02023e59bb268d68a71fa1951607a687333a0aca 100644
--- a/src/plugins/reduc/dune-project
+++ b/src/plugins/reduc/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/report/dune-project b/src/plugins/report/dune-project
index a85c40cebfa957990bdb76d898e0cd33df11caf6..f0306f7eaa7ca6d2e82a4385c70fb37a8754fde7 100644
--- a/src/plugins/report/dune-project
+++ b/src/plugins/report/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/rte/dune-project b/src/plugins/rte/dune-project
index 1087951f653046357a2763ceecb68da034298446..13e6264437c97d10bc7c7f8fe87759b25afe6802 100644
--- a/src/plugins/rte/dune-project
+++ b/src/plugins/rte/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/scope/dune-project b/src/plugins/scope/dune-project
index 8c7953c33276f34b30138afdf96d41c0c5a40e89..f35ceb4834c646c0f1f57e43ee0cc2572eed0d2c 100644
--- a/src/plugins/scope/dune-project
+++ b/src/plugins/scope/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/security_slicing/dune-project b/src/plugins/security_slicing/dune-project
index 73b3bfee2513861eca727b9147db61eaa55638ea..4bf4c106a698abd74d03c962ea2077749207ccb4 100644
--- a/src/plugins/security_slicing/dune-project
+++ b/src/plugins/security_slicing/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index a0bde444c1f17c1b2fb92f69a5a83e51948f25b8..e88927103f77c3ca79c14e6e775dafecf8b942bd 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -368,11 +368,11 @@ sig
end
(** Builds an indexer that {i does not} depend on current project. *)
-module Static(M : Map)(I : Info) :
+module Static(M : Map)(_ : Info) :
Index with type t = M.key and type tag := int
(** Builds a {i projectified} index. *)
-module Index(M : Map)(I : Info) :
+module Index(M : Map)(_ : Info) :
Index with type t = M.key and type tag := int
(** Datatype already identified by unique integers. *)
@@ -383,7 +383,7 @@ sig
end
(** Builds a {i projectified} index on types with {i unique} identifiers. *)
-module Identified(A : IdentifiedType)(I : Info) :
+module Identified(A : IdentifiedType)(_ : Info) :
Index with type t = A.t and type tag := int
(** Datatype already identified by unique integers. *)
@@ -394,7 +394,7 @@ sig
end
(** Builds a {i projectified} index on types with {i unique} identifiers. *)
-module Tagged(A : TaggedType)(I : Info) :
+module Tagged(A : TaggedType)(_ : Info) :
Index with type t = A.t and type tag := string
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/dune-project b/src/plugins/server/dune-project
index 864472bae72a5e58bba090f72805e151aa7499af..f73b2da04b8b19c53ecf77e48d3ddaabd3b58aac 100644
--- a/src/plugins/server/dune-project
+++ b/src/plugins/server/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/slicing/dune-project b/src/plugins/slicing/dune-project
index 3c67d5396ded345be7611a622565dc940b638cc0..7b55b8d077a491676c1b2ed144ff5992b0146f5a 100644
--- a/src/plugins/slicing/dune-project
+++ b/src/plugins/slicing/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/sparecode/dune-project b/src/plugins/sparecode/dune-project
index 526b4997ab7d827949e7359def2b957a959e714e..873e175b801ef64f7bd055559e3a5f684c6d1cc9 100644
--- a/src/plugins/sparecode/dune-project
+++ b/src/plugins/sparecode/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/studia/dune-project b/src/plugins/studia/dune-project
index 1fb45865162b7a212f06d5f9e2eba44988a963b7..afe3133659b446e5cefa7bbe2ba59e97e88a6579 100644
--- a/src/plugins/studia/dune-project
+++ b/src/plugins/studia/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/users/dune-project b/src/plugins/users/dune-project
index de808f5c12f61f43c3f960ef56187e1c78aba22f..b2d79d60cc45f9c801792e907492ef027c2309b2 100644
--- a/src/plugins/users/dune-project
+++ b/src/plugins/users/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/variadic/dune-project b/src/plugins/variadic/dune-project
index 8de451bcef19ab19ed265b0b0e235faa017bd5ce..49f444baf72690488ee0d1728fbb3a02f9251b2b 100644
--- a/src/plugins/variadic/dune-project
+++ b/src/plugins/variadic/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/wp/MemDebug.mli b/src/plugins/wp/MemDebug.mli
index dca97a279721145906d448b8e26aee6af6190d29..856d1084a22c2b40448ced3983e4e416681db1d4 100644
--- a/src/plugins/wp/MemDebug.mli
+++ b/src/plugins/wp/MemDebug.mli
@@ -35,4 +35,4 @@ val pp_rloc : 'a Pretty_utils.formatter -> Format.formatter ->
val pp_sloc : 'a Pretty_utils.formatter -> Format.formatter ->
'a Sigs.sloc -> unit
-module Make(M : Sigs.Model) : Sigs.Model
+module Make(_ : Sigs.Model) : Sigs.Model
diff --git a/src/plugins/wp/MemVal.mli b/src/plugins/wp/MemVal.mli
index 96a89a399ac78bd4e381853579d36d17de1f204d..7e71f55246e6617a2ecca51bb9a88d6c1556ed92 100644
--- a/src/plugins/wp/MemVal.mli
+++ b/src/plugins/wp/MemVal.mli
@@ -88,7 +88,7 @@ sig
val pretty : Format.formatter -> t -> unit
end
-module Make(V : Value) : Sigs.Model
+module Make(_ : Value) : Sigs.Model
(** The glue between WP and EVA. **)
module Eva : Value
diff --git a/src/plugins/wp/MemVar.mli b/src/plugins/wp/MemVar.mli
index 75d459b41491d4cffe8399741c05d7a055239af9..b899ff59aa574329816d443d325fe4cce7a0bfa8 100644
--- a/src/plugins/wp/MemVar.mli
+++ b/src/plugins/wp/MemVar.mli
@@ -42,4 +42,4 @@ module Raw : VarUsage
module Static : VarUsage
(** Create a mixed Hoare Memory Model from VarUsage instance. *)
-module Make(V : VarUsage)(M : Sigs.Model) : Sigs.Model
+module Make(_ : VarUsage)(_ : Sigs.Model) : Sigs.Model
diff --git a/src/plugins/wp/dune-project b/src/plugins/wp/dune-project
index fb6fa24ce8ed1c3a612e0bc39c06e168d288d73c..03706f9a1cca4b70b1c51cc1fbcc7ee8d8fb8603 100644
--- a/src/plugins/wp/dune-project
+++ b/src/plugins/wp/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 091d61aa6b9332112d3ecb196e0a9c620810a591..472469818eda9f6d9faeec430db6253d73493d3a 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -493,9 +493,9 @@ let do_list_scheduled_result () =
type script = {
mutable proverscript : bool ;
mutable strategies : bool ;
- mutable scratch : bool ;
- mutable update : bool ;
- mutable stdout : bool ;
+ scratch : bool ;
+ update : bool ;
+ stdout : bool ;
mutable depth : int ;
mutable width : int ;
mutable backtrack : int ;
diff --git a/tools/hdrck/dune-project b/tools/hdrck/dune-project
index c27d657559687bced36fa7e44e8eecc60f45d10c..bc13dab0fcc32652187b959f3b3051b74801ce27 100644
--- a/tools/hdrck/dune-project
+++ b/tools/hdrck/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/tools/lint/dune-project b/tools/lint/dune-project
index 23b0e5a01616310ddedad826f70cc4edb706d0a4..803d09ccdffd650c88d1255a093bf7da444b2f0e 100644
--- a/tools/lint/dune-project
+++ b/tools/lint/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/tools/ptests/dune-project b/tools/ptests/dune-project
index 475e7f1d70b73480ec6785ac45704d07091f6de0..c5e576885d9cbe1ef6ab8f961c177334aeb1540d 100644
--- a/tools/ptests/dune-project
+++ b/tools/ptests/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.2)
+(lang dune 3.3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/tools/ptests/ptests.ml b/tools/ptests/ptests.ml
index 4d1178925e63237b512ff43158d4324c99ae0070..09da1de670727ed031afbcc89632eeb14909e42a 100644
--- a/tools/ptests/ptests.ml
+++ b/tools/ptests/ptests.ml
@@ -40,7 +40,6 @@ type env_t = {
config: string
; dir: string
; dune_alias: string
-; absolute_tests_dir: string
; absolute_cwd: string
}
@@ -610,7 +609,6 @@ type execnow =
{ ex_cmd: string; (** command to launch *)
ex_log: string list; (** log files *)
ex_bin: string list; (** bin files *)
- ex_dir: SubDir.t; (** directory of test suite *)
ex_timeout: string;
ex_deps: deps;
ex_exit_code: string option
@@ -631,7 +629,6 @@ type cmd = {
type config =
{
- dc_subdir: SubDir.t ;
dc_test_regexp: string; (** regexp of test files. *)
dc_execnow : execnow list; (** command to be launched before
the toplevel(s)
@@ -727,9 +724,8 @@ end = struct
timeout=""
} ]
- let default_config dir =
- { dc_subdir = dir;
- dc_test_regexp = test_file_regexp;
+ let default_config () =
+ { dc_test_regexp = test_file_regexp;
dc_macros = Macros.default_macros ();
dc_execnow = [];
dc_libs = None;
@@ -749,7 +745,7 @@ end = struct
dc_timeout = "";
}
- let scan_execnow ~file ~once dir ex_exit_code ex_timeout ex_deps (s:string) =
+ let scan_execnow ~file ~once ex_exit_code ex_timeout ex_deps (s:string) =
if once=false then
Format.eprintf "%s: using EXEC directive (DEPRECATED): %s@."
file s;
@@ -781,7 +777,6 @@ end = struct
{ ex_cmd = s;
ex_log = [];
ex_bin = [];
- ex_dir = dir;
ex_deps;
ex_timeout;
ex_exit_code;
@@ -831,11 +826,11 @@ end = struct
enabled_if = select ~prev:deps.enabled_if ~config:config.dc_enabled_if
}
- let config_exec ~once ~drop:_ ~file ~dir s current =
+ let config_exec ~once ~drop:_ ~file s current =
let s = Macros.expand ~file current.dc_macros s in
{ current with
dc_execnow =
- scan_execnow ~file ~once dir
+ scan_execnow ~file ~once
current.dc_exit_code current.dc_timeout (deps_of_config current)
s :: current.dc_execnow
}
@@ -917,14 +912,12 @@ end = struct
end
type parsing_env = {
- current_default_toplevel: string;
current_default_log: string list;
current_default_bin: string list;
current_default_cmds: cmd list;
}
let default_parsing_env = ref {
- current_default_toplevel = "" ;
current_default_log = [] ;
current_default_bin = [] ;
current_default_cmds = []
@@ -932,7 +925,6 @@ end = struct
let set_default_parsing_env config =
default_parsing_env := {
- current_default_toplevel = config.dc_default_toplevel;
current_default_log = config.dc_default_log;
current_default_bin = config.dc_default_bin;
current_default_cmds = List.rev config.dc_commands;
@@ -1024,8 +1016,12 @@ end = struct
(fun ~drop:_ ~file:_ ~dir:_ _ current ->
{ current with dc_dont_run = true });
- "EXECNOW", config_exec ~once:true;
- "EXEC", config_exec ~once:false;
+ "EXECNOW",
+ (fun ~drop ~file ~dir:_ s acc ->
+ config_exec ~once:true ~file ~drop s acc);
+ "EXEC",
+ (fun ~drop ~file ~dir:_ s acc ->
+ config_exec ~once:false ~file ~drop s acc);
"MACRO", config_macro;
"LIBS", config_libs;
@@ -1093,7 +1089,7 @@ end = struct
(* test for a possible toplevel configuration. *)
let current_config ~env dir =
- let default_config = default_config dir in
+ let default_config = default_config () in
let general_config_file = SubDir.make_file dir (config_name ~env filename) in
if Sys.file_exists general_config_file
then begin
@@ -1941,13 +1937,6 @@ let test_pattern config =
let regexp = Str.regexp config.dc_test_regexp in
fun file -> Str.string_match regexp file 0
-(* if we have some references to directories in the default config, they
- need to be adapted to the actual test directory. *)
-let update_dir_ref dir config =
- let update_execnow e = { e with ex_dir = dir } in
- let dc_execnow = List.map update_execnow config.dc_execnow in
- { config with dc_execnow }
-
let build_modules fmt modules =
(* Prints rules dedicated to the build of the MODULEs *)
let n = ref 0 in
@@ -2111,10 +2100,6 @@ let () =
let absolute_cwd = Unix.getcwd () in
List.iter (fun dir ->
Format.printf "Test directory: %s@." dir;
- let absolute_tests_dir = Filename.dirname
- (if Filename.is_relative dir
- then Filename.concat absolute_cwd dir else dir)
- in
let suites = Ptests_config.parse ~dir in
if !verbosity >= 1 then Format.printf "%% Nb config= %d@." (StringMap.cardinal suites);
let nb = !nb_dune_files in
@@ -2128,10 +2113,9 @@ let () =
| _ ->
if !verbosity >= 1 then Format.printf "%% - %s_SUITES -> nb suites= %d@."
(match config_mode with "" -> default_config | s -> s) (StringMap.cardinal suites);
- let env = { config = config_mode ; dir ; dune_alias = "" ; absolute_tests_dir ; absolute_cwd} in
+ let env = { config = config_mode ; dir ; dune_alias = "" ; absolute_cwd} in
let directory = SubDir.create ~with_subdir:false ~env dir in
let config = Test_config.current_config ~env directory in
- let config = update_dir_ref directory config in
process ~env config suites) suites ;
let nbi = !nb_ignores in
if !verbosity >= 1 then Format.printf "%% Nb dune files= %d@." (!nb_dune_files-nb);