From 96f3dbd362c0ad93fbbd62ced0014b1d1ed53dd5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 30 Jan 2020 16:31:04 +0100
Subject: [PATCH] [stdlib] Removes FCMap, und uses stdlib Map instead.
---
.Makefile.lint | 2 -
Makefile | 1 -
src/kernel_internals/typing/mergecil.ml | 2 +-
src/kernel_services/ast_data/annotations.ml | 2 +-
.../ast_queries/logic_typing.ml | 2 +-
src/libraries/datatype/datatype.ml | 6 +-
src/libraries/datatype/datatype.mli | 4 +-
src/libraries/stdlib/FCHashtbl.ml | 2 +-
src/libraries/stdlib/FCMap.ml | 76 -------
src/libraries/stdlib/FCMap.mli | 199 ------------------
src/libraries/stdlib/transitioning.ml.in | 1 +
src/libraries/stdlib/transitioning.mli | 1 +
src/plugins/from/from_register.ml | 2 +-
src/plugins/metrics/metrics_base.ml | 2 +-
src/plugins/metrics/metrics_base.mli | 2 +-
src/plugins/security_slicing/components.ml | 2 +-
src/plugins/value/gui_files/gui_types.ml | 2 +-
src/plugins/value/gui_files/gui_types.mli | 2 +-
src/plugins/wp/Cint.ml | 2 +-
src/plugins/wp/Factory.ml | 2 +-
src/plugins/wp/Letify.ml | 2 +-
src/plugins/wp/Splitter.ml | 2 +-
src/plugins/wp/Warning.ml | 2 +-
src/plugins/wp/Warning.mli | 2 +-
src/plugins/wp/cfgWP.ml | 2 +-
src/plugins/wp/cil2cfg.ml | 2 +-
src/plugins/wp/clabels.mli | 2 +-
src/plugins/wp/register.ml | 2 +-
src/plugins/wp/wpContext.ml | 6 +-
src/plugins/wp/wpReport.ml | 2 +-
src/plugins/wp/wpo.ml | 2 +-
src/plugins/wp/wpo.mli | 2 +-
32 files changed, 33 insertions(+), 309 deletions(-)
delete mode 100644 src/libraries/stdlib/FCMap.ml
delete mode 100644 src/libraries/stdlib/FCMap.mli
diff --git a/.Makefile.lint b/.Makefile.lint
index af170b508da..259a202aa40 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -149,8 +149,6 @@ ML_LINT_KO+=src/libraries/project/state_topological.mli
ML_LINT_KO+=src/libraries/stdlib/FCBuffer.ml
ML_LINT_KO+=src/libraries/stdlib/FCBuffer.mli
ML_LINT_KO+=src/libraries/stdlib/FCHashtbl.mli
-ML_LINT_KO+=src/libraries/stdlib/FCMap.ml
-ML_LINT_KO+=src/libraries/stdlib/FCMap.mli
ML_LINT_KO+=src/libraries/stdlib/FCSet.ml
ML_LINT_KO+=src/libraries/stdlib/FCSet.mli
ML_LINT_KO+=src/libraries/stdlib/extlib.ml
diff --git a/Makefile b/Makefile
index d8e4d6405e5..b9150c02477 100644
--- a/Makefile
+++ b/Makefile
@@ -441,7 +441,6 @@ CMO += $(VERY_FIRST_CMO)
LIB_CMO =\
src/libraries/stdlib/transitioning \
src/libraries/stdlib/FCSet \
- src/libraries/stdlib/FCMap \
src/libraries/stdlib/FCBuffer \
src/libraries/stdlib/FCHashtbl \
src/libraries/stdlib/extlib \
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 7db861b0dbd..d8b6f886817 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -171,7 +171,7 @@ struct
(* Find the representative for a node and compress the paths in the process *)
module Heq = Hashtbl.Make (Elts)
- module Iter_sorted = FCMap.Make(Elts)
+ module Iter_sorted = Map.Make(Elts)
module Hsyn = Hashtbl.Make(H)
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 684fcea7ce2..d8c0fefc98c 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -280,7 +280,7 @@ let merge_funspec s1 s2 =
(** {2 Getting annotations} *)
(**************************************************************************)
-module StmtContractMap = FCMap.Make(Datatype.String.Set)
+module StmtContractMap = Transitioning.Stdlib.Map.Make(Datatype.String.Set)
let is_same_behavior_set l1 l2 =
Datatype.String.Set.(equal (of_list l1) (of_list l2))
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index e8fa630ffaf..4d6d1f1947f 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -310,7 +310,7 @@ let binop_of_rel = function
module Lenv = struct
(* locals: logic variables (e.g. quantified variables in \forall, \exists) *)
- module Smap = FCMap.Make(String)
+ module Smap = Map.Make(String)
type t = {
local_vars: Cil_types.logic_var Smap.t;
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 417d5f8ea37..cddbeb78d57 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -294,7 +294,7 @@ module type Set = sig
end
module type Map = sig
- include FCMap.S
+ include Map.S
module Key: S with type t = key
module Make(Data: S) : S with type t = Data.t t
end
@@ -1433,7 +1433,7 @@ end
(* ****************************************************************************)
module Map
- (M: FCMap.S)(Key: S with type t = M.key)(Info: Functor_info) =
+ (M: Map.S)(Key: S with type t = M.key)(Info: Functor_info) =
struct
let () = check Key.equal "equal" Key.name Info.module_name
@@ -1677,7 +1677,7 @@ module With_collections(X: S)(Info: Functor_info) = struct
module Map =
Map
- (FCMap.Make(D))
+ (Transitioning.Stdlib.Map.Make(D))
(D)
(struct let module_name = Info.module_name ^ ".Map" end)
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 9d659f95aaa..bf25151f44c 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -240,7 +240,7 @@ end
(** A standard OCaml map signature extended with datatype operations. *)
module type Map = sig
- include FCMap.S
+ include Map.S
module Key: S with type t = key
(** Datatype for the keys of the map. *)
@@ -638,7 +638,7 @@ module Set
Set with type t = S.t and type elt = E.t
module Map
- (M: FCMap.S)(Key: S with type t = M.key)(Info: Functor_info) :
+ (M: Map.S)(Key: S with type t = M.key)(Info: Functor_info) :
Map with type 'a t = 'a M.t and type key = M.key and module Key = Key
module Hashtbl
diff --git a/src/libraries/stdlib/FCHashtbl.ml b/src/libraries/stdlib/FCHashtbl.ml
index a19c31b5996..00a6463e5da 100644
--- a/src/libraries/stdlib/FCHashtbl.ml
+++ b/src/libraries/stdlib/FCHashtbl.ml
@@ -52,7 +52,7 @@ module Make(H: Hashtbl.HashedType) : S with type key = H.t = struct
let fold_sorted ?(cmp=Transitioning.Stdlib.compare) f h acc =
let module Aux = struct type t = key let compare = cmp end in
- let module M = FCMap.Make(Aux) in
+ let module M = Map.Make(Aux) in
let add k v m =
try
let l = v :: M.find k m in
diff --git a/src/libraries/stdlib/FCMap.ml b/src/libraries/stdlib/FCMap.ml
deleted file mode 100644
index 9df135bf3bc..00000000000
--- a/src/libraries/stdlib/FCMap.ml
+++ /dev/null
@@ -1,76 +0,0 @@
-(*****************************************************************************)
-(* *)
-(* This file was originally part of Objective Caml *)
-(* *)
-(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
-(* *)
-(* Copyright (C) 1996 INRIA *)
-(* INRIA (Institut National de Recherche en Informatique et en *)
-(* Automatique) *)
-(* *)
-(* All rights reserved. *)
-(* *)
-(* This file is distributed under the terms of the GNU Library General *)
-(* Public License version 2, with the special exception on linking *)
-(* described below. See the GNU Library General Public License version *)
-(* 2 for more details (enclosed in the file licenses/LGPLv2). *)
-(* *)
-(* As a special exception to the GNU Library General Public License, *)
-(* you may link, statically or dynamically, a "work that uses the Library" *)
-(* with a publicly distributed version of the Library to *)
-(* produce an executable file containing portions of the Library, and *)
-(* distribute that executable file under terms of your choice, without *)
-(* any of the additional requirements listed in clause 6 of the GNU *)
-(* Library General Public License. *)
-(* By "a publicly distributed version of the Library", *)
-(* we mean either the unmodified Library as *)
-(* distributed by INRIA, or a modified version of the Library that is *)
-(* distributed under the conditions defined in clause 2 of the GNU *)
-(* Library General Public License. This exception does not however *)
-(* invalidate any other reasons why the executable file might be *)
-(* covered by the GNU Library General Public License. *)
-(* *)
-(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
-(* énergies alternatives). *)
-(* *)
-(*****************************************************************************)
-
-module type S =
- sig
- type key
- type +'a t
- val empty: 'a t
- val is_empty: 'a t -> bool
- val mem: key -> 'a t -> bool
- val add: key -> 'a -> 'a t -> 'a t
- val singleton: key -> 'a -> 'a t
- val remove: key -> 'a t -> 'a t
- val merge: (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
- val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
- val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
- val iter: (key -> 'a -> unit) -> 'a t -> unit
- val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
- val for_all: (key -> 'a -> bool) -> 'a t -> bool
- val exists: (key -> 'a -> bool) -> 'a t -> bool
- val filter: (key -> 'a -> bool) -> 'a t -> 'a t
- val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
- val cardinal: 'a t -> int
- val bindings: 'a t -> (key * 'a) list
- val min_binding: 'a t -> (key * 'a)
- val max_binding: 'a t -> (key * 'a)
- val choose: 'a t -> (key * 'a)
- val split: key -> 'a t -> 'a t * 'a option * 'a t
- val find: key -> 'a t -> 'a
- val find_opt: key -> 'a t -> 'a option
- val map: ('a -> 'b) -> 'a t -> 'b t
- val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
- end
-
-
-module Make(X: Map.OrderedType) = struct
- include Map.Make(X)
- let find_opt k m =
- match find k m with
- | exception Not_found -> None
- | v -> Some v
-end
diff --git a/src/libraries/stdlib/FCMap.mli b/src/libraries/stdlib/FCMap.mli
deleted file mode 100644
index edaad5e5bb5..00000000000
--- a/src/libraries/stdlib/FCMap.mli
+++ /dev/null
@@ -1,199 +0,0 @@
-(*****************************************************************************)
-(* *)
-(* This file was originally part of Objective Caml *)
-(* *)
-(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
-(* *)
-(* Copyright (C) 1996 INRIA *)
-(* INRIA (Institut National de Recherche en Informatique et en *)
-(* Automatique) *)
-(* *)
-(* All rights reserved. *)
-(* *)
-(* This file is distributed under the terms of the GNU Library General *)
-(* Public License version 2, with the special exception on linking *)
-(* described below. See the GNU Library General Public License version *)
-(* 2 for more details (enclosed in the file licenses/LGPLv2). *)
-(* *)
-(* As a special exception to the GNU Library General Public License, *)
-(* you may link, statically or dynamically, a "work that uses the Library" *)
-(* with a publicly distributed version of the Library to *)
-(* produce an executable file containing portions of the Library, and *)
-(* distribute that executable file under terms of your choice, without *)
-(* any of the additional requirements listed in clause 6 of the GNU *)
-(* Library General Public License. *)
-(* By "a publicly distributed version of the Library", *)
-(* we mean either the unmodified Library as *)
-(* distributed by INRIA, or a modified version of the Library that is *)
-(* distributed under the conditions defined in clause 2 of the GNU *)
-(* Library General Public License. This exception does not however *)
-(* invalidate any other reasons why the executable file might be *)
-(* covered by the GNU Library General Public License. *)
-(* *)
-(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
-(* énergies alternatives). *)
-(* *)
-(*****************************************************************************)
-
-(** Association tables over ordered types.
-
- This signatures is a partial copy of the signature of [Map.S] of
- OCaml's standard library, which we extend with some new functions.
-*)
-
-module type S =
- sig
- type key
- (** The type of the map keys. *)
-
- type (+'a) t
- (** The type of maps from type [key] to type ['a]. *)
-
- val empty: 'a t
- (** The empty map. *)
-
- val is_empty: 'a t -> bool
- (** Test whether a map is empty or not. *)
-
- val mem: key -> 'a t -> bool
- (** [mem x m] returns [true] if [m] contains a binding for [x],
- and [false] otherwise. *)
-
- val add: key -> 'a -> 'a t -> 'a t
- (** [add x y m] returns a map containing the same bindings as
- [m], plus a binding of [x] to [y]. If [x] was already bound
- in [m], its previous binding disappears. *)
-
- val singleton: key -> 'a -> 'a t
- (** [singleton x y] returns the one-element map that contains a binding [y]
- for [x].
- @since 3.12.0
- *)
-
- val remove: key -> 'a t -> 'a t
- (** [remove x m] returns a map containing the same bindings as
- [m], except for [x] which is unbound in the returned map. *)
-
- val merge:
- (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
- (** [merge f m1 m2] computes a map whose keys is a subset of keys of [m1]
- and of [m2]. The presence of each such binding, and the corresponding
- value, is determined with the function [f].
- @since 3.12.0
- *)
-
- val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
- (** Total ordering between maps. The first argument is a total ordering
- used to compare data associated with equal keys in the two maps. *)
-
- val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
- (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are
- equal, that is, contain equal keys and associate them with
- equal data. [cmp] is the equality predicate used to compare
- the data associated with the keys. *)
-
- val iter: (key -> 'a -> unit) -> 'a t -> unit
- (** [iter f m] applies [f] to all bindings in map [m].
- [f] receives the key as first argument, and the associated value
- as second argument. The bindings are passed to [f] in increasing
- order with respect to the ordering over the type of the keys. *)
-
- val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
- (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)],
- where [k1 ... kN] are the keys of all bindings in [m]
- (in increasing order), and [d1 ... dN] are the associated data. *)
-
- val for_all: (key -> 'a -> bool) -> 'a t -> bool
- (** [for_all p m] checks if all the bindings of the map
- satisfy the predicate [p].
- @since 3.12.0
- *)
-
- val exists: (key -> 'a -> bool) -> 'a t -> bool
- (** [exists p m] checks if at least one binding of the map
- satisfy the predicate [p].
- @since 3.12.0
- *)
-
- val filter: (key -> 'a -> bool) -> 'a t -> 'a t
- (** [filter p m] returns the map with all the bindings in [m]
- that satisfy predicate [p].
- @since 3.12.0
- *)
-
- val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
- (** [partition p m] returns a pair of maps [(m1, m2)], where
- [m1] contains all the bindings of [s] that satisfy the
- predicate [p], and [m2] is the map with all the bindings of
- [s] that do not satisfy [p].
- @since 3.12.0
- *)
-
- val cardinal: 'a t -> int
- (** Return the number of bindings of a map.
- @since 3.12.0
- *)
-
- val bindings: 'a t -> (key * 'a) list
- (** Return the list of all bindings of the given map.
- The returned list is sorted in increasing order with respect
- to the ordering [Ord.compare], where [Ord] is the argument
- given to {!Map.Make}.
- @since 3.12.0
- *)
-
- val min_binding: 'a t -> (key * 'a)
- (** Return the smallest binding of the given map
- (with respect to the [Ord.compare] ordering), or raise
- [Not_found] if the map is empty.
- @since 3.12.0
- *)
-
- val max_binding: 'a t -> (key * 'a)
- (** Same as {!min_binding}, but returns the largest binding
- of the given map.
- @since 3.12.0
- *)
-
- val choose: 'a t -> (key * 'a)
- (** Return one binding of the given map, or raise [Not_found] if
- the map is empty. Which binding is chosen is unspecified,
- but equal bindings will be chosen for equal maps.
- @since 3.12.0
- *)
-
- val split: key -> 'a t -> 'a t * 'a option * 'a t
- (** [split x m] returns a triple [(l, data, r)], where
- [l] is the map with all the bindings of [m] whose key
- is strictly less than [x];
- [r] is the map with all the bindings of [m] whose key
- is strictly greater than [x];
- [data] is [None] if [m] contains no binding for [x],
- or [Some v] if [m] binds [v] to [x].
- @since 3.12.0
- *)
-
- val find: key -> 'a t -> 'a
- (** [find x m] returns the current binding of [x] in [m],
- or raises [Not_found] if no such binding exists. *)
-
- val find_opt: key -> 'a t -> 'a option
- (** [find x m] returns the current binding of [x] in [m],
- or return [None] if no such binding exists. *)
-
- val map: ('a -> 'b) -> 'a t -> 'b t
- (** [map f m] returns a map with same domain as [m], where the
- associated value [a] of all bindings of [m] has been
- replaced by the result of the application of [f] to [a].
- The bindings are passed to [f] in increasing order
- with respect to the ordering over the type of the keys. *)
-
- val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
- (** Same as {!map}, but the function receives as arguments both the
- key and the associated value for each binding of the map. *)
-
- end
-
-module Make (Ord : Map.OrderedType) : S with type key = Ord.t
-(** Functor building an implementation of the map structure
- given a totally ordered type. *)
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index f9f3b85e50c..8ceacaa401a 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -30,6 +30,7 @@ module Stdlib = struct
let min_int = min_int
let max_int = max_int
let flush = flush
+ module Map = Map
end
[@@@ warning "-3"]
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index 6e75b7538ad..5ae8e71271b 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -43,6 +43,7 @@ module Stdlib: sig
val min_int: int
val max_int: int
val flush: out_channel -> unit
+ module Map: module type of Map
end
(** 4.08 *)
diff --git a/src/plugins/from/from_register.ml b/src/plugins/from/from_register.ml
index a94fe66d894..92f856fc209 100644
--- a/src/plugins/from/from_register.ml
+++ b/src/plugins/from/from_register.ml
@@ -58,7 +58,7 @@ module SortCalls = struct
good criterion is left *)
else r
end
-module MapStmtCalls = FCMap.Make(SortCalls)
+module MapStmtCalls = Map.Make(SortCalls)
let iter_callwise_calls_sorted f =
let hkf = Kernel_function.Hashtbl.create 17 in
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index b55a6772f17..bc1d8b63d55 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -269,7 +269,7 @@ module VarinfoByName = struct
end
(** Map and sets of varinfos sorted by name (and not by ids) *)
-module VInfoMap = FCMap.Make (VarinfoByName)
+module VInfoMap = Map.Make (VarinfoByName)
module VInfoSet = FCSet.Make (VarinfoByName)
diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli
index 9ff77090ef5..c344b1c0ce6 100644
--- a/src/plugins/metrics/metrics_base.mli
+++ b/src/plugins/metrics/metrics_base.mli
@@ -96,7 +96,7 @@ end
(** Local varinfo map and set where the comparison function is the
lexicographic one on their respective names. *)
-module VInfoMap: FCMap.S with type key = Cil_types.varinfo
+module VInfoMap: Map.S with type key = Cil_types.varinfo
module VInfoSet: FCSet.S with type elt = Cil_types.varinfo
;;
diff --git a/src/plugins/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index d126b3dfeb4..0395492fd10 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -291,7 +291,7 @@ module Component = struct
(* not optimal implementation: no memoization (bts#006) *)
- module M = FCMap.Make(NodeKf)
+ module M = Map.Make(NodeKf)
type fwd_kind = Impact | Security
diff --git a/src/plugins/value/gui_files/gui_types.ml b/src/plugins/value/gui_files/gui_types.ml
index f4fad0001bc..48ad75465a0 100644
--- a/src/plugins/value/gui_files/gui_types.ml
+++ b/src/plugins/value/gui_files/gui_types.ml
@@ -46,7 +46,7 @@ let compare_gui_callstack cs1 cs2 = match cs1, cs2 with
| _, GC_Single _ -> 1
| GC_Single _, _ -> -1
-module GCallstackMap = FCMap.Make(struct
+module GCallstackMap = Map.Make(struct
type t = gui_callstack
let compare = compare_gui_callstack
end)
diff --git a/src/plugins/value/gui_files/gui_types.mli b/src/plugins/value/gui_files/gui_types.mli
index 538247fa92d..dd82f8e8b05 100644
--- a/src/plugins/value/gui_files/gui_types.mli
+++ b/src/plugins/value/gui_files/gui_types.mli
@@ -29,7 +29,7 @@ type gui_callstack =
val hash_gui_callstack : gui_callstack -> int
val compare_gui_callstack : gui_callstack -> gui_callstack -> int
-module GCallstackMap : FCMap.S with type key = gui_callstack
+module GCallstackMap : Map.S with type key = gui_callstack
type gui_selection =
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 4329cdf81c5..7866b2d1414 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -28,7 +28,7 @@ open Qed
open Qed.Logic
open Lang
open Lang.F
-module FunMap = FCMap.Make(Lang.Fun)
+module FunMap = Map.Make(Lang.Fun)
(* -------------------------------------------------------------------------- *)
(* --- Kernel Interface --- *)
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 3fde0d76ebc..b5c2ffc5797 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -300,7 +300,7 @@ let configure_driver setup driver () =
(* --- Access --- *)
(* -------------------------------------------------------------------------- *)
-module COMPILERS = FCMap.Make
+module COMPILERS = Map.Make
(struct
type t = setup * driver
let compare (s,d) (s',d') =
diff --git a/src/plugins/wp/Letify.ml b/src/plugins/wp/Letify.ml
index 309456f6f91..c9a07102c81 100644
--- a/src/plugins/wp/Letify.ml
+++ b/src/plugins/wp/Letify.ml
@@ -439,7 +439,7 @@ struct
(* --- Pretty --- *)
- module Xmap = FCMap.Make(Var)
+ module Xmap = Map.Make(Var)
let pretty title fmt sigma =
let def = Vmap.fold Xmap.add sigma.def Xmap.empty in
diff --git a/src/plugins/wp/Splitter.ml b/src/plugins/wp/Splitter.ml
index c7afbd32731..ef4cbb45634 100644
--- a/src/plugins/wp/Splitter.ml
+++ b/src/plugins/wp/Splitter.ml
@@ -143,7 +143,7 @@ module Tags = Qed.Listset.Make
let equal x y = (compare x y = 0)
end)
module M = Qed.Listmap.Make(Tags)
-module I = FCMap.Make(Tags)
+module I = Map.Make(Tags)
type 'a t = 'a M.t
diff --git a/src/plugins/wp/Warning.ml b/src/plugins/wp/Warning.ml
index e9bc3d515bf..78f631fba1f 100644
--- a/src/plugins/wp/Warning.ml
+++ b/src/plugins/wp/Warning.ml
@@ -53,7 +53,7 @@ struct
end
include SELF
-module Map = FCMap.Make(SELF)
+module Map = Map.Make(SELF)
module Set = FCSet.Make(SELF)
let severe s = Set.exists (fun w -> w.severe) s
diff --git a/src/plugins/wp/Warning.mli b/src/plugins/wp/Warning.mli
index aab4aaf2381..0ba5dc048f9 100644
--- a/src/plugins/wp/Warning.mli
+++ b/src/plugins/wp/Warning.mli
@@ -40,7 +40,7 @@ val compare : t -> t -> int
val pretty : Format.formatter -> t -> unit
module Set : FCSet.S with type elt = t
-module Map : FCMap.S with type key = t
+module Map : Map.S with type key = t
val severe : Set.t -> bool
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 5c9f650ca85..565431efa06 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1279,7 +1279,7 @@ struct
(* -------------------------------------------------------------------------- *)
(* NOTE: bug in ocamldoc in OCaml 4.02 prevents usage of 'P' here *)
- module PMAP = FCMap.Make(WpPropId.PropId)
+ module PMAP = Map.Make(WpPropId.PropId)
type group = {
mutable verifs : VC_Annot.t Bag.t ;
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index 3129f581006..d009c01f040 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -225,7 +225,7 @@ end
module PMAP(X: Graph.Sig.COMPARABLE) = struct
- module M = FCMap.Make(X)
+ module M = Map.Make(X)
type 'a t = 'a M.t ref
type key = X.t
type 'a return = unit
diff --git a/src/plugins/wp/clabels.mli b/src/plugins/wp/clabels.mli
index 0a8ada54b2b..ae01c683374 100644
--- a/src/plugins/wp/clabels.mli
+++ b/src/plugins/wp/clabels.mli
@@ -36,7 +36,7 @@ val mem : c_label -> c_label list -> bool
val equal : c_label -> c_label -> bool
module T : sig type t = c_label val compare : t -> t -> int end
-module LabelMap : FCMap.S with type key = c_label
+module LabelMap : Map.S with type key = c_label
module LabelSet : FCSet.S with type elt = c_label
val pre : c_label
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index e2371df94b2..5ee0a232c14 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -195,7 +195,7 @@ let do_wpo_display goal =
Wp_parameters.feedback "Goal %s : %s" (Wpo.get_gid goal) result
module PM =
- FCMap.Make(struct
+ Map.Make(struct
type t = VCS.prover
let compare = VCS.cmp_prover
end)
diff --git a/src/plugins/wp/wpContext.ml b/src/plugins/wp/wpContext.ml
index fda8f5d01b3..98f6832b2a1 100644
--- a/src/plugins/wp/wpContext.ml
+++ b/src/plugins/wp/wpContext.ml
@@ -192,7 +192,7 @@ let freetype a =
with Not_found ->
Hashtbl.add types a 1 ; a
-module NAMES = FCMap.Make(String)
+module NAMES = Map.Make(String)
module Index(E : Entries) =
struct
@@ -203,7 +203,7 @@ struct
type data = E.data
module KEY = struct type t = E.key let compare = E.compare end
- module MAP = FCMap.Make(KEY)
+ module MAP = Map.Make(KEY)
module SET = FCSet.Make(KEY)
let demon = ref []
@@ -338,7 +338,7 @@ struct
type data = E.data
module KEY = struct type t = E.key let compare = E.compare end
- module MAP = FCMap.Make(KEY)
+ module MAP = Map.Make(KEY)
module SET = FCSet.Make(KEY)
let demon = ref []
diff --git a/src/plugins/wp/wpReport.ml b/src/plugins/wp/wpReport.ml
index f4b201c3b7e..4769a676fef 100644
--- a/src/plugins/wp/wpReport.ml
+++ b/src/plugins/wp/wpReport.ml
@@ -290,7 +290,7 @@ let decode_chapter= function
| Axiom _ -> "axiomatic"
| Fun _ -> "function"
-module Smap = FCMap.Make
+module Smap = Map.Make
(struct
type t = entry
let compare s1 s2 =
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 35dc0735338..514a16f7426 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -549,7 +549,7 @@ end
module WPOset = WpoType.Set
module WPOmap = WpoType.Map
-module Gmap = FCMap.Make(Index)
+module Gmap = Map.Make(Index)
module Fmap = Kernel_function.Map
module Pmap = Property.Map
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index aba0f8ad7d6..4035da3f2f7 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -115,7 +115,7 @@ type po = t and t = {
module S : Datatype.S_with_collections with type t = po
module Index : Map.OrderedType with type t = index
-module Gmap : FCMap.S with type key = index
+module Gmap : Map.S with type key = index
(** Dynamically exported
@since Nitrogen-20111001
--
GitLab