From 770f0f279b5aec743ecb55124876bf096b7eeb05 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 11 May 2022 08:31:19 +0200
Subject: [PATCH] [kernel] Datatype : no more varname (no more journal)
---
.../abstract_interp/abstract_interp.ml | 6 --
src/kernel_services/abstract_interp/base.ml | 2 -
.../abstract_interp/int_Base.ml | 2 +-
.../abstract_interp/int_interval.ml | 2 +-
.../abstract_interp/int_set.ml | 2 +-
.../abstract_interp/int_val.ml | 2 +-
src/kernel_services/abstract_interp/ival.ml | 2 +-
src/kernel_services/abstract_interp/lmap.ml | 2 +-
.../abstract_interp/lmap_bitwise.ml | 2 +-
.../abstract_interp/map_lattice.ml | 2 +-
.../abstract_interp/offsetmap.ml | 3 +-
src/kernel_services/abstract_interp/origin.ml | 2 +-
src/kernel_services/ast_data/alarms.ml | 2 +-
.../ast_data/property_status.ml | 1 -
src/kernel_services/ast_queries/ast_diff.ml | 7 --
.../ast_queries/cil_builtins.ml | 1 -
.../ast_queries/cil_datatype.ml | 82 +++++++++----------
.../cmdline_parameters/typed_parameter.ml | 2 +-
.../plugin_entry_points/emitter.ml | 4 +-
src/libraries/datatype/datatype.ml | 69 ----------------
src/libraries/datatype/datatype.mli | 16 ----
src/libraries/project/project.ml | 1 -
src/libraries/project/state.ml | 2 +-
src/libraries/utils/hptmap.ml | 2 +-
src/libraries/utils/rangemap.ml | 2 +-
src/plugins/aorai/data_for_aorai.ml | 6 +-
.../e-acsl/src/analyses/analyses_datatype.ml | 2 +-
src/plugins/obfuscator/obfuscator_kind.ml | 2 +-
src/plugins/pdg_types/pdgTypes.ml | 2 +-
src/plugins/slicing/Slicing.mli | 0
src/plugins/slicing/slicingTypes.ml | 6 +-
.../value/partitioning/split_strategy.ml | 2 +-
src/plugins/value/values/offsm_value.ml | 2 +-
src/plugins/value_types/cvalue.ml | 2 +-
src/plugins/value_types/function_Froms.ml | 6 +-
src/plugins/wp/Lang.ml | 2 +-
src/plugins/wp/ctypes.ml | 2 +-
src/plugins/wp/wpPropId.ml | 2 +-
38 files changed, 71 insertions(+), 185 deletions(-)
mode change 100644 => 100755 src/plugins/slicing/Slicing.mli
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 0569d8fe257..80cc2545356 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -223,7 +223,6 @@ module Make_Generic_Lattice_Set
let rehash = Datatype.identity
let copy = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end) :
Datatype.S with type t := t)
@@ -364,7 +363,6 @@ module Make_Lattice_Base (V:Lattice_Value):(Lattice_Base with type l = V.t) = st
let rehash = Datatype.identity
let copy = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end) :
Datatype.S with type t := t)
@@ -515,7 +513,6 @@ module Bool = struct
let rehash = Datatype.identity
let copy = Datatype.identity
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end) :
Datatype.S with type t := t)
@@ -675,7 +672,6 @@ struct
let rehash = Datatype.identity
let copy = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end) :
Datatype.S with type t := t)
@@ -774,7 +770,6 @@ struct
let rehash = Datatype.identity
let copy = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end):
Datatype.S with type t := t)
@@ -943,7 +938,6 @@ struct
let rehash = Datatype.undefined
let copy = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
let () = Type.set_ml_name ty None
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 4734eef3706..e0b94048054 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -101,7 +101,6 @@ module Validity = Datatype.Make
let mem_project = Datatype.never_any_project
let rehash = Datatype.identity
let copy (x:t) = x
- let varname _ = "v"
end)
type cstring = CSString of string | CSWstring of Escape.wstring
@@ -451,7 +450,6 @@ module Base = struct
let mem_project = Datatype.never_any_project
let rehash = Datatype.identity
let copy = Datatype.undefined
- let varname = Datatype.undefined
end)
let id = id
let pretty_debug = pretty
diff --git a/src/kernel_services/abstract_interp/int_Base.ml b/src/kernel_services/abstract_interp/int_Base.ml
index f75a06568c3..fe28f63e41c 100644
--- a/src/kernel_services/abstract_interp/int_Base.ml
+++ b/src/kernel_services/abstract_interp/int_Base.ml
@@ -56,7 +56,7 @@ include Datatype.Make
let rehash = Datatype.identity
let copy = Extlib.id
let pretty = pretty
- let varname = Datatype.undefined
+
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index 4900196abcd..f6cd553dac2 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -96,7 +96,7 @@ include Datatype.Make_with_collections
let rehash = Datatype.identity
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
- let varname = Datatype.undefined
+
end)
(* ------------------------------ Building ---------------------------------- *)
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index e1fe0de0590..474944295db 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -132,7 +132,7 @@ include Datatype.Make_with_collections
let rehash x = x
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
- let varname = Datatype.undefined
+
end)
(* ---------------------------------- Utils --------------------------------- *)
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 424ba043ea0..23f49a22f59 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -77,7 +77,7 @@ include Datatype.Make_with_collections
let rehash x = x
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
- let varname = Datatype.undefined
+
end)
(* ------------------------------- Constructors ---------------------------- *)
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 233c6f19fc2..ac2cec82d0e 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -826,7 +826,7 @@ include (
let rehash = rehash
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
- let varname = Datatype.undefined
+
end):
Datatype.S_with_collections with type t := t)
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 483210b3835..063250f501c 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -593,7 +593,7 @@ struct
let pretty = pretty
let rehash = Datatype.identity
let copy = Datatype.undefined
- let varname = Datatype.undefined
+
let mem_project = Datatype.never_any_project
end)
let () = Type.set_ml_name ty None
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.ml b/src/kernel_services/abstract_interp/lmap_bitwise.ml
index 72515172d0e..ea853b5e86d 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.ml
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml
@@ -240,7 +240,7 @@ struct
let pretty = pretty
let rehash = Datatype.identity
let copy = Datatype.undefined
- let varname = Datatype.undefined
+
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 0d0d31d9e90..caec2966924 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/src/kernel_services/abstract_interp/map_lattice.ml
@@ -500,7 +500,7 @@ module Make_MapSet_Lattice
let copy = Datatype.undefined
let pretty = pretty
let mem_project = Datatype.never_any_project
- let varname = Datatype.undefined
+
end): Datatype.S_with_collections with type t := t)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 0bc43658600..ed8d1b9080b 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -230,7 +230,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
let rehash x = !rehash_ref x
let copy = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
+
let mem_project = Datatype.never_any_project
end)
include D
@@ -2459,7 +2459,6 @@ module Int_Intervals = struct
Int.packed_descr; Int.packed_descr |] |]
let mem_project = Datatype.never_any_project
- let varname _ = "i"
let copy = Datatype.undefined
end)
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index c6cdb0fd21c..4603d837ecd 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -136,7 +136,7 @@ include Datatype.Make
let rehash = Datatype.undefined
let copy = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
+
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 3ccb9304cb3..1878a37f634 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -240,7 +240,7 @@ module D =
let structural_descr = Structural_descr.t_abstract
let rehash = Datatype.identity
- let varname = Datatype.undefined
+
let pretty fmt = function
| Division_by_zero e ->
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index ba440a42ed5..46c82aeca51 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -80,7 +80,6 @@ module Emitter_with_properties =
let copy = Datatype.undefined
let pretty fmt e = Usable_emitter.pretty fmt e.emitter
- let varname _ = assert false
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 96a1eb0a076..ffa3ca42bd6 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -62,9 +62,6 @@ struct
let mk_pretty pp fmt = function
| `Not_present -> Format.pp_print_string fmt "N/A"
| `Same x -> Format.fprintf fmt " => %a" pp x
- let mk_varname v = function
- | `Not_present -> "x"
- | `Same x -> v x ^ "_c"
let mk_mem_project mem query = function
| `Not_present -> false
| `Same x -> mem query x
@@ -157,10 +154,6 @@ struct
Format.fprintf fmt "-> %a %a" pp x pretty_pc flags
| #correspondance as x -> Correspondance_input.mk_pretty pp fmt x
- let mk_varname f = function
- | `Partial (x,_) -> f x ^ "_pc"
- | #correspondance as x -> Correspondance_input.mk_varname f x
-
let mk_mem_project f p = function
| `Partial (x,_) -> f p x
| #correspondance as x -> Correspondance_input.mk_mem_project f p x
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index 8d224fd39bf..9a825e39a8e 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -168,7 +168,6 @@ module Builtin_template = struct
let rehash = Datatype.identity
let structural_descr = Structural_descr.t_abstract
let mem_project = Datatype.never_any_project
- let varname b = "_cb_" ^ b.name
end)
end
module Builtin_templates =
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 3e9dfcb0c49..8dfc722a6cf 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -49,7 +49,6 @@ module Make
val name: string
val reprs: t list
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
end) =
Datatype.Make
(struct
@@ -69,7 +68,6 @@ module Make_with_collections
val compare: t -> t -> int
val equal: t -> t -> bool
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
val hash: t -> int
val copy: t -> t
end) =
@@ -158,7 +156,6 @@ module Cabs_file = struct
let name = "Cabs_file"
let reprs = [ Datatype.Filepath.dummy, [];
Datatype.Filepath.dummy, [ true, Cabs.GLOBANNOT [] ] ]
- let varname (s, _) = "cabs_" ^ (Filepath.Normalized.to_pretty_string s)
let pretty fmt cabs = !pretty_ref fmt cabs
end)
end
@@ -197,7 +194,7 @@ module Position = struct
let copy = Datatype.identity
let equal: t -> t -> bool = ( = )
let pretty = Filepath.pp_pos
- let varname _ = "pos"
+
end)
let pp_with_col fmt pos =
Format.fprintf fmt "%a char %d" pretty pos
@@ -221,7 +218,7 @@ module Location = struct
let copy = Datatype.identity (* immutable strings *)
let equal : t -> t -> bool = ( = )
let pretty fmt loc = !pretty_ref fmt loc
- let varname _ = "loc"
+
end)
let pretty_long fmt loc =
@@ -270,7 +267,7 @@ module Instr = struct
let name = "Instr"
let reprs = List.map (fun l -> Skip l) Location.reprs
let pretty fmt x = !pretty_ref fmt x
- let varname = Datatype.undefined
+
end)
let loc = function
@@ -294,7 +291,7 @@ module File =
globinit = None;
globinitcalled = false } ]
include Datatype.Undefined
- let varname _ = "ast"
+
end)
module Stmt_Id = struct
@@ -316,7 +313,7 @@ module Stmt_Id = struct
let equal t1 t2 = t1.sid = t2.sid
let copy = Datatype.undefined
let pretty fmt s = !pretty_ref fmt s
- let varname _ = "stmt"
+
end)
let id stmt = stmt.sid
end
@@ -369,7 +366,7 @@ module Kinstr = struct
| Kglobal ->
Format.fprintf fmt "Kglobal"
| Kstmt s -> Stmt.pretty fmt s
- let varname _ = "ki"
+
end)
let loc = function
@@ -596,7 +593,6 @@ module Attribute=struct
let equal = Datatype.from_compare
let copy = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
- let varname = Datatype.undefined
end)
end
@@ -620,7 +616,7 @@ struct
let equal = Datatype.from_compare
let copy = Datatype.undefined
let pretty fmt t = !pretty_typ_ref fmt t
- let varname = Datatype.undefined
+
end)
end
@@ -713,7 +709,7 @@ module Label = struct
let reprs =
[ Label("", Location.unknown, false); Default Location.unknown ]
let pretty fmt l = !pretty_ref fmt l
- let varname = Datatype.undefined
+
let hash = function
| Default _ -> 7
| Case (e, _) -> Exp.hash e
@@ -773,7 +769,6 @@ module Varinfo_Id = struct
let equal v1 v2 = v1.vid = v2.vid
let copy = Datatype.undefined
let pretty fmt v = !pretty_ref fmt v
- let varname v = "vi_" ^ v.vorig_name
end)
let id v = v.vid
end
@@ -809,7 +804,7 @@ module Compinfo = struct
let equal v1 v2 = v1.ckey = v2.ckey
let copy = Datatype.undefined
let pretty fmt f = !pretty_ref fmt f
- let varname = Datatype.undefined
+
end)
end
@@ -851,7 +846,7 @@ module Fieldinfo = struct
let equal f1 f2 = (fid f1) = (fid f2)
let copy = Datatype.undefined
let pretty fmt f = !pretty_ref fmt f
- let varname = Datatype.undefined
+
end)
end
@@ -1127,7 +1122,7 @@ module Block = struct
[{battrs=[]; blocals=Varinfo.reprs; bstatics = [];
bstmts=Stmt.reprs; bscoping=true}]
let pretty fmt b = !pretty_ref fmt b
- let varname = Datatype.undefined
+
end)
let equal b1 b2 = (b1 == b2)
end
@@ -1195,7 +1190,7 @@ module Lval = struct
let hash = hash_lval
let copy = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "lv"
+
end)
end
@@ -1210,7 +1205,7 @@ module LvalStructEq_input = struct
let hash = StructEq.hash_lval 13598
let copy = Datatype.undefined
let pretty fmt x = !Lval.pretty_ref fmt x
- let varname _ = "lv"
+
end
module LvalStructEq = Make_compare_non_strict(LvalStructEq_input)
@@ -1229,7 +1224,7 @@ module Offset = struct
let hash = hash_offset
let copy = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "offs"
+
end)
end
@@ -1244,7 +1239,7 @@ module OffsetStructEq_input = struct
let hash = StructEq.hash_offset 75489
let copy = Datatype.undefined
let pretty fmt x = !Offset.pretty_ref fmt x
- let varname _ = "offs"
+
end
module OffsetStructEq = Make_compare_non_strict(OffsetStructEq_input)
@@ -1278,7 +1273,7 @@ module Logic_var = struct
let equal v1 v2 = v1.lv_id = v2.lv_id
let copy = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
- let varname _ = "logic_var"
+
end)
end
@@ -1299,7 +1294,7 @@ module Builtin_logic_info = struct
let equal i1 i2 = i1.bl_name = i2.bl_name
let copy = Datatype.identity (* works only if an AST is never modified *)
let pretty fmt li = !pretty_ref fmt li
- let varname = Datatype.undefined
+
end)
end
@@ -1316,7 +1311,7 @@ module Logic_type_info = struct
let hash t = Hashtbl.hash t.lt_name
let copy = Datatype.identity (* works only if an AST is never modified *)
let pretty fmt lt = !pretty_ref fmt lt
- let varname = Datatype.undefined
+
end)
end
@@ -1335,7 +1330,7 @@ module Logic_ctor_info = struct
let hash t = Hashtbl.hash t.ctor_name
let copy = Datatype.identity (* works only if an AST is never modified *)
let pretty fmt c = !pretty_ref fmt c
- let varname = Datatype.undefined
+
end)
end
@@ -1349,7 +1344,7 @@ module Initinfo = struct
{ init = None } ::
List.map (fun t -> { init = Some (CompoundInit(t, [])) }) Typ.reprs
let pretty fmt i = !pretty_ref fmt i
- let varname = Datatype.undefined
+
end)
end
@@ -1374,7 +1369,7 @@ module Logic_info = struct
let hash i = Logic_var.hash i.l_var_info
let copy = Datatype.undefined
let pretty fmt li = !pretty_ref fmt li
- let varname _ = "logic_varinfo"
+
end)
end
@@ -1458,7 +1453,7 @@ module Logic_info_structural = struct
let hash i = Logic_var.hash i.l_var_info
let copy = Datatype.undefined
let pretty fmt li = !Logic_info.pretty_ref fmt li
- let varname _ = "logic_varinfo"
+
end)
end
@@ -2044,7 +2039,7 @@ module Logic_constant = struct
let hash = hash_logic_constant
let copy = Datatype.undefined
let pretty fmt lc = !pretty_ref fmt lc
- let varname _ = "lconst"
+
end)
end
@@ -2067,7 +2062,7 @@ module Term = struct
let copy = Datatype.undefined
let hash = hash_fct hash_term
let pretty fmt t = !pretty_ref fmt t
- let varname _ = "term"
+
end)
end
@@ -2086,7 +2081,7 @@ module Identified_term = struct
{ it_id = x.it_id; it_content = Term.copy x.it_content }
let hash x = x.it_id
let pretty fmt t = !pretty_ref fmt t
- let varname _ = "id_term"
+
end)
end
@@ -2110,7 +2105,7 @@ module Term_lhost = struct
let hash = hash_fct hash_tlhost
let copy = Datatype.undefined
let pretty fmt h = !pretty_ref fmt h
- let varname = Datatype.undefined
+
end)
end
@@ -2126,7 +2121,7 @@ module Term_offset = struct
let hash = hash_fct hash_toffset
let copy = Datatype.undefined
let pretty fmt t_o = !pretty_ref fmt t_o
- let varname = Datatype.undefined
+
end)
end
@@ -2153,7 +2148,7 @@ module Logic_label = struct
let copy = Datatype.undefined
let hash = hash_label
let pretty fmt l = !pretty_ref fmt l
- let varname _ = "logic_label"
+
end)
end
@@ -2173,7 +2168,7 @@ module Logic_real = struct
let equal r1 r2 = compare r1 r2 = 0
let copy = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
- let varname _ = "logic_real"
+
end)
end
@@ -2185,7 +2180,7 @@ module Global_annotation = struct
let name = "Global_annotation"
let reprs = List.map (fun l -> Daxiomatic ("", [],[], l)) Location.reprs
let pretty fmt v = !pretty_ref fmt v
- let varname = Datatype.undefined
+
let rec compare g1 g2 =
match g1,g2 with
@@ -2275,7 +2270,7 @@ module Global = struct
let name = "Global"
let reprs = [ GText "" ]
let pretty fmt v = !pretty_ref fmt v
- let varname = Datatype.undefined
+
let compare g1 g2 =
match g1, g2 with
@@ -2428,10 +2423,8 @@ module Kf = struct
| Declaration (_, v, Some args, _) ->
!set_formal_decls v args;
x
- let get_name_kf kf = (vi kf).Cil_types.vname
let pretty fmt kf = Varinfo.pretty fmt (vi kf)
let mem_project = Datatype.never_any_project
- let varname kf = "kf_" ^ (get_name_kf kf)
end)
let () = Type.set_ml_name ty (Some "Kernel_function.ty")
@@ -2452,7 +2445,7 @@ module Code_annotation = struct
let compare x y = Datatype.Int.compare x.annot_id y.annot_id
let copy = Datatype.undefined
let pretty fmt ca = !pretty_ref fmt ca
- let varname _ = "code_annot"
+
end)
let loc ca = match ca.annot_content with
@@ -2475,7 +2468,7 @@ module Predicate = struct
pred_loc = Location.unknown;
pred_content = Pfalse } ]
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "p"
+
end)
end
@@ -2488,7 +2481,7 @@ module Toplevel_predicate = struct
let reprs =
[ { tp_statement = List.hd Predicate.reprs; tp_kind = Assert }]
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "p"
+
end)
end
@@ -2505,7 +2498,7 @@ module Identified_predicate = struct
let copy = Datatype.undefined
let hash x = x.ip_id
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "id_predyes"
+
end)
end
@@ -2524,7 +2517,7 @@ module PredicateStructEq = struct
let copy = Datatype.undefined
let hash = hash_fct hash_predicate
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "p"
+
end)
end
@@ -2590,7 +2583,6 @@ module Fundec = struct
(struct
type t = fundec
let name = "Fundec"
- let varname v = "fd_" ^ v.svar.vorig_name
let reprs = reprs
let structural_descr = Structural_descr.t_abstract
let compare v1 v2 = Datatype.Int.compare v1.svar.vid v2.svar.vid
@@ -2616,7 +2608,7 @@ module Lexpr = Make
let name = "Lexpr"
let reprs = [ { lexpr_node = PLvar ""; lexpr_loc = Location.unknown } ]
let pretty = Datatype.undefined (* TODO *)
- let varname = Datatype.undefined
+
end)
(**************************************************************************)
diff --git a/src/kernel_services/cmdline_parameters/typed_parameter.ml b/src/kernel_services/cmdline_parameters/typed_parameter.ml
index 8a9e8f585ac..7d25ed3ce65 100644
--- a/src/kernel_services/cmdline_parameters/typed_parameter.ml
+++ b/src/kernel_services/cmdline_parameters/typed_parameter.ml
@@ -67,7 +67,7 @@ include
let hash x = Datatype.String.hash x.name
let copy x = x (* The representation of the parameter is immutable *)
let pretty fmt x = Format.pp_print_string fmt x.name
- let varname _ = assert false
+
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml
index fd379811e41..63cd6fade34 100644
--- a/src/kernel_services/plugin_entry_points/emitter.ml
+++ b/src/kernel_services/plugin_entry_points/emitter.ml
@@ -103,7 +103,7 @@ module D =
let hash x = Datatype.String.hash x.name
let copy x = x (* strings are immutable here *)
let pretty fmt x = Format.pp_print_string fmt x.name
- let varname _ = assert false
+
let mem_project = Datatype.never_any_project
end)
@@ -147,7 +147,7 @@ module Usable_emitter = struct
Format.fprintf fmt "%s (v%d)" name x.version
else
Format.pp_print_string fmt name
- let varname _ = assert false
+
let mem_project = Datatype.never_any_project
end)
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 9ae247627df..73a64e23699 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -30,7 +30,6 @@ type 'a t =
hash: 'a -> int;
copy: 'a -> 'a;
pretty: Format.formatter -> 'a -> unit;
- varname: 'a -> string;
mem_project: (Project_skeleton.t -> bool) -> 'a -> bool }
type 'a info = 'a t
@@ -50,7 +49,6 @@ module type S_no_copy = sig
val compare: t -> t -> int
val hash: t -> int
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
end
@@ -79,7 +77,6 @@ let compare ty = (internal_info "compare" ty).compare
let hash ty = (internal_info "hash" ty).hash
let copy ty = (internal_info "copy" ty).copy
let pretty ty = (internal_info "pretty" ty).pretty
-let varname ty = (internal_info "varname" ty).varname
let mem_project ty = (internal_info "mem_project" ty).mem_project
let info ty = internal_info "info" ty
@@ -101,7 +98,6 @@ module type Undefined = sig
val rehash: 'a -> 'a
val copy: 'a -> 'a
val pretty: Format.formatter -> 'a -> unit
- val varname: 'a -> string
val mem_project: (Project_skeleton.t -> bool) -> 'a -> bool
end
@@ -111,7 +107,6 @@ module Partial_undefined = struct
let hash = undefined
let copy = undefined
let pretty = undefined
- let varname = undefined
let mem_project = undefined
end
@@ -132,11 +127,6 @@ end
(** {2 Generic builders} *)
(* ********************************************************************** *)
-let valid_varname s =
- let r = Str.regexp "[^A-Za-z0-9_]+" in
- let s = Str.global_replace r "__" s in
- String.uncapitalize_ascii s
-
let check f fname tname fstr =
assert
(if f == undefined && Type.may_use_obj () then begin
@@ -158,7 +148,6 @@ module Build
val rehash: t -> t
val copy: t -> t
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
end) =
struct
@@ -174,13 +163,7 @@ struct
let hash = T.hash
let rehash = T.rehash
let copy = T.copy
-
let pretty = T.pretty
-
- let varname =
- if T.varname == undefined then undefined
- else fun x -> valid_varname (T.varname x)
-
let mem_project = T.mem_project
let info =
@@ -189,7 +172,6 @@ struct
hash = hash;
copy = copy;
pretty = pretty;
- varname = varname;
mem_project = mem_project }
let () = Infos.add info_tbl T.ty info
@@ -232,7 +214,6 @@ module type Make_input = sig
val hash: t -> int
val copy: t -> t
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
end
@@ -325,7 +306,6 @@ module type Polymorphic2_input = sig
val mk_pretty:
(Format.formatter -> 'a -> unit) -> (Format.formatter -> 'b -> unit) ->
Format.formatter -> ('a, 'b) t -> unit
- val mk_varname: ('a -> string) -> ('b -> string) -> ('a, 'b) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -389,7 +369,6 @@ module Polymorphic2(P: Polymorphic2_input) = struct
in
build mk T1.copy T2.copy
let pretty = build P.mk_pretty T1.pretty T2.pretty
- let varname = build P.mk_varname T1.varname T2.varname
let mem_project =
let mk f1 f2 =
if P.mk_mem_project == undefined then undefined
@@ -439,9 +418,6 @@ module Polymorphic3
(Format.formatter -> 'b -> unit) ->
(Format.formatter -> 'c -> unit) ->
Format.formatter -> ('a, 'b, 'c) t -> unit
- val mk_varname:
- ('a -> string) -> ('b -> string) -> ('c -> string) ->
- ('a, 'b, 'c) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -509,7 +485,6 @@ struct
in
build mk T1.copy T2.copy T3.copy
let pretty = build P.mk_pretty T1.pretty T2.pretty T3.pretty
- let varname = build P.mk_varname T1.varname T2.varname T3.varname
let mem_project =
let mk f1 f2 f3 =
if P.mk_mem_project == undefined then undefined
@@ -570,9 +545,6 @@ module Polymorphic4
(Format.formatter -> 'c -> unit) ->
(Format.formatter -> 'd -> unit) ->
Format.formatter -> ('a, 'b, 'c, 'd) t -> unit
- val mk_varname:
- ('a -> string) -> ('b -> string) -> ('c -> string) -> ('d -> string) ->
- ('a, 'b, 'c, 'd) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -644,8 +616,6 @@ struct
in
build mk T1.copy T2.copy T3.copy T4.copy
let pretty = build P.mk_pretty T1.pretty T2.pretty T3.pretty T4.pretty
- let varname =
- build P.mk_varname T1.varname T2.varname T3.varname T4.varname
let mem_project =
let mk f1 f2 f3 f4 =
if P.mk_mem_project == undefined then undefined
@@ -694,7 +664,6 @@ module Pair_arg = struct
let mk_pretty f1 f2 fmt (x1, x2) =
let pp fmt = Format.fprintf fmt "@[<hv 2>%a,@;%a@]" f1 x1 f2 x2 in
Type.par Type.Basic Type.Tuple fmt pp
- let mk_varname = undefined
let mk_mem_project mem1 mem2 f (x1, x2) = mem1 f x1 && mem2 f x2
end
@@ -742,7 +711,6 @@ let pair (type typ1) (type typ2) (ty1: typ1 Type.t) (ty2: typ2 Type.t) =
let hash = hash X.ty
let copy = copy X.ty
let pretty = pretty X.ty
- let varname = varname ty
let mem_project = mem_project X.ty
end
in
@@ -769,7 +737,6 @@ struct
let rehash = undefined
let copy = undefined
let pretty = undefined
- let varname _ = "f"
let mem_project = never_any_project
let reprs =
if Type.may_use_obj () then Type.reprs ty else [ fun _ -> assert false ]
@@ -811,7 +778,6 @@ module type Polymorphic_input = sig
val map: ('a -> 'a) -> 'a t -> 'a t
val mk_pretty:
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
- val mk_varname: ('a -> string) -> 'a t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
(Project_skeleton.t -> bool) -> 'a t -> bool
@@ -875,7 +841,6 @@ module Polymorphic_gen(P: Polymorphic_input) = struct
fun x -> P.map X.copy x
let rehash = R.rehash
let pretty = build P.mk_pretty X.pretty
- let varname = build P.mk_varname X.varname
let mem_project =
let mk f =
if P.mk_mem_project == undefined then undefined
@@ -926,7 +891,6 @@ module Poly_ref =
let mk_pretty f fmt x =
let pp fmt = Format.fprintf fmt "@[<hv 2>ref@;%a@]" f !x in
Type.par Type.Basic Type.Call fmt pp
- let mk_varname = undefined
let mk_mem_project mem f x = mem f !x
end)
@@ -946,7 +910,6 @@ let t_ref (type typ) (ty: typ Type.t) =
let hash = hash ty
let copy = copy ty
let pretty = pretty ty
- let varname = varname ty
let mem_project = mem_project ty
end)
in
@@ -985,7 +948,6 @@ module Poly_option =
Format.fprintf fmt "@[<hv 2>Some@;%a@]" f x
in
Type.par Type.Basic Type.Call fmt pp
- let mk_varname = undefined
let mk_mem_project mem f = function None -> false | Some x -> mem f x
end)
@@ -1006,7 +968,6 @@ let option (type typ) (ty: typ Type.t) =
let hash = hash ty
let copy = copy ty
let pretty = pretty ty
- let varname = varname ty
let mem_project = mem_project ty
end)
in
@@ -1059,7 +1020,6 @@ module Poly_list =
print fmt l)
in
Type.par Type.Basic Type.Basic fmt pp (* Never enclose lists in parentheses *)
- let mk_varname = undefined
let mk_mem_project mem f = List.exists (mem f)
end)
@@ -1080,7 +1040,6 @@ let list (type typ) (ty: typ Type.t) =
let hash = hash ty
let copy = copy ty
let pretty = pretty ty
- let varname = varname ty
let mem_project = mem_project ty
end)
in
@@ -1144,7 +1103,6 @@ module Poly_array =
done))
in
Type.par Type.Basic Type.Basic fmt pp (* Never enclose arrays in parentheses *)
- let mk_varname = undefined
let mk_mem_project mem f a =
try
for i = 0 to (Array.length a - 1) do
@@ -1170,7 +1128,6 @@ let array (type typ) (ty: typ Type.t) =
let hash = hash ty
let copy = copy ty
let pretty = pretty ty
- let varname = varname ty
let mem_project = mem_project ty
end)
in
@@ -1198,7 +1155,6 @@ module Poly_queue =
let mk_hash = undefined
let map = undefined
let mk_pretty = undefined
- let mk_varname = undefined
let mk_mem_project mem f q =
try Queue.iter (fun x -> if mem f x then raise Exit) q; false
with Exit -> true
@@ -1220,7 +1176,6 @@ let queue (type typ) (ty: typ Type.t) =
let hash = hash ty
let copy = copy ty
let pretty = pretty ty
- let varname = varname ty
let mem_project = mem_project ty
end)
in
@@ -1273,7 +1228,6 @@ struct
~pre:"@[<hov 2>{@ " ~sep:";@ " ~suf:"@ }@]"
S.iter (pp_elt E.pretty) fmt s
- let varname = undefined
let mem_project p s =
try S.iter (fun x -> if E.mem_project p x then raise Exit) s; false
with Exit -> true
@@ -1294,7 +1248,6 @@ struct
let compare = P.compare
let hash = P.hash
let pretty = P.pretty
- let varname = P.varname
let mem_project = P.mem_project
let copy = P.copy
@@ -1335,9 +1288,6 @@ struct
f_value v)
map;
Format.fprintf fmt " }}@]"
- let mk_varname _ =
- if Key.varname == undefined then undefined
- else fun _ -> Format.sprintf "%s_map" Key.name
let mk_mem_project =
if Key.mem_project == undefined then undefined
else
@@ -1416,7 +1366,6 @@ struct
H.iter (fun k v -> H.add h2 k v) h;
h2
let mk_pretty = undefined
- let mk_varname = undefined
let mk_mem_project =
if Key.mem_project == undefined then undefined
else
@@ -1572,7 +1521,6 @@ module Simple_type
val reprs: t list
val pretty: Format.formatter -> t -> unit
val copy: t -> t
- val varname: t -> string
val compare: t -> t -> int
val equal: t -> t -> bool
end) =
@@ -1592,7 +1540,6 @@ struct
let rehash = identity
let copy = X.copy
let pretty = X.pretty
- let varname = X.varname
let mem_project = never_any_project
end))
(struct let module_name = module_name end)
@@ -1611,7 +1558,6 @@ module Unit =
let compare () () = 0
let equal () () = true
let pretty fmt () = Format.fprintf fmt "()"
- let varname = undefined
end)
let unit = Unit.ty
@@ -1625,7 +1571,6 @@ module Bool =
let compare : bool -> bool -> int = Stdlib.compare
let equal : bool -> bool -> bool = (=)
let pretty fmt b = Format.fprintf fmt "%B" b
- let varname _ = "b"
end)
let bool = Bool.ty
@@ -1639,7 +1584,6 @@ module Int = struct
let compare : int -> int -> int = Stdlib.compare
let equal : int -> int -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%d" n
- let varname _ = "n"
end)
let compare : int -> int -> int = Stdlib.compare
end
@@ -1655,7 +1599,6 @@ module Int32 =
let compare = Int32.compare
let equal : int32 -> int32 -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%ld" n
- let varname _ = "n32"
end)
let int32 = Int32.ty
@@ -1669,7 +1612,6 @@ module Int64 =
let compare = Int64.compare
let equal : int64 -> int64 -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%Ld" n
- let varname _ = "n64"
end)
let int64 = Int64.ty
@@ -1683,7 +1625,6 @@ module Nativeint =
let compare = Nativeint.compare
let equal : nativeint -> nativeint -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%nd" n
- let varname _ = "native_n"
end)
let nativeint = Nativeint.ty
@@ -1697,7 +1638,6 @@ module Float =
let compare : float -> float -> int = Stdlib.compare
let equal : float -> float -> bool = (=)
let pretty fmt f = Format.fprintf fmt "%f" f
- let varname _ = "f"
end)
let float = Float.ty
@@ -1711,7 +1651,6 @@ module Char =
let compare = Char.compare
let equal : char -> char -> bool = (=)
let pretty fmt c = Format.fprintf fmt "%c" c
- let varname _ = "c"
end)
let char = Char.ty
@@ -1725,7 +1664,6 @@ module String =
let compare = String.compare
let equal : string -> string -> bool = (=)
let pretty fmt s = Format.fprintf fmt "%S" s
- let varname _ = "s"
end)
let string = String.ty
@@ -1742,7 +1680,6 @@ module Formatter =
let rehash = undefined
let copy = undefined
let pretty = undefined
- let varname _ = "fmt"
let mem_project = never_any_project
end)
let formatter = Formatter.ty
@@ -1761,7 +1698,6 @@ module Integer =
let copy = identity
(* TODO: this should take into account kernel's option -big-ints-hex *)
let pretty = Integer.pretty
- let varname _ = "integer_n"
let mem_project = never_any_project
end)
let integer = Integer.ty
@@ -1776,7 +1712,6 @@ module Filepath = struct
let compare = Filepath.Normalized.compare
let equal : t -> t -> bool = (=)
let pretty = Filepath.Normalized.pretty
- let varname _ = "p"
end)
let dummy = Filepath.Normalized.empty
let of_string ?existence ?base_name s =
@@ -1814,7 +1749,6 @@ module Triple_arg = struct
Format.fprintf fmt "@[<hv 2>%a,@;%a,@;%a@]" f1 x1 f2 x2 f3 x3
in
Type.par Type.Basic Type.Tuple fmt pp
- let mk_varname = undefined
let mk_mem_project mem1 mem2 mem3 f (x1, x2, x3) =
mem1 f x1 && mem2 f x2 && mem3 f x3
end
@@ -1866,7 +1800,6 @@ let triple
let hash = hash X.ty
let copy = copy X.ty
let pretty = pretty X.ty
- let varname = varname ty
let mem_project = mem_project X.ty
end
in
@@ -1912,7 +1845,6 @@ module Quadruple_arg = struct
Format.fprintf fmt "@[<hv 2>%a,@;%a,@;%a,@;%a@]" f1 x1 f2 x2 f3 x3 f4 x4
in
Type.par Type.Basic Type.Tuple fmt pp
- let mk_varname = undefined
let mk_mem_project mem1 mem2 mem3 mem4 f (x1, x2, x3, x4) =
mem1 f x1 && mem2 f x2 && mem3 f x3 && mem4 f x4
end
@@ -1969,7 +1901,6 @@ let quadruple
let hash = hash X.ty
let copy = copy X.ty
let pretty = pretty X.ty
- let varname = varname ty
let mem_project = mem_project X.ty
end
in
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 057a592dff5..6f06777de1f 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -37,7 +37,6 @@ type 'a t = private
hash: 'a -> int;
copy: 'a -> 'a;
pretty: Format.formatter -> 'a -> unit;
- varname: 'a -> string;
mem_project: (Project_skeleton.t -> bool) -> 'a -> bool }
(** A type with its type value. *)
@@ -75,10 +74,6 @@ module type S_no_copy = sig
val pretty: Format.formatter -> t -> unit
(** Pretty print each value in an user-friendly way. *)
- val varname: t -> string
- (** A good prefix name to use for an OCaml variable of this type. Only useful
- for journalisation. *)
-
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
(** [mem_project f x] must return [true] iff there is a value [p] of type
[Project.t] in [x] such that [f p] returns [true]. *)
@@ -102,7 +97,6 @@ val compare: 'a Type.t -> 'a -> 'a -> int
val hash: 'a Type.t -> 'a -> int
val copy: 'a Type.t -> 'a -> 'a
val pretty: 'a Type.t -> Format.formatter -> 'a -> unit
-val varname: 'a Type.t -> 'a -> string
val mem_project: 'a Type.t -> (Project_skeleton.t -> bool) -> 'a -> bool
(* ********************************************************************** *)
@@ -137,7 +131,6 @@ module type Undefined = sig
val rehash: 'a -> 'a
val copy: 'a -> 'a
val pretty: Format.formatter -> 'a -> unit
- val varname: 'a -> string
val mem_project: (Project_skeleton.t -> bool) -> 'a -> bool
end
@@ -193,7 +186,6 @@ module type Make_input = sig
val hash: t -> int
val copy: t -> t
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
end
@@ -352,7 +344,6 @@ module Polymorphic
val map: ('a -> 'a) -> 'a t -> 'a t
val mk_pretty:
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
- val mk_varname: ('a -> string) -> 'a t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
(Project_skeleton.t -> bool) -> 'a t -> bool
@@ -380,7 +371,6 @@ module Polymorphic2
val mk_pretty:
(Format.formatter -> 'a -> unit) -> (Format.formatter -> 'b -> unit) ->
Format.formatter -> ('a, 'b) t -> unit
- val mk_varname: ('a -> string) -> ('b -> string) -> ('a, 'b) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -417,9 +407,6 @@ module Polymorphic3
(Format.formatter -> 'b -> unit) ->
(Format.formatter -> 'c -> unit) ->
Format.formatter -> ('a, 'b, 'c) t -> unit
- val mk_varname:
- ('a -> string) -> ('b -> string) -> ('c -> string) ->
- ('a, 'b, 'c) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -463,9 +450,6 @@ module Polymorphic4
(Format.formatter -> 'c -> unit) ->
(Format.formatter -> 'd -> unit) ->
Format.formatter -> ('a, 'b, 'c, 'd) t -> unit
- val mk_varname:
- ('a -> string) -> ('b -> string) -> ('c -> string) -> ('d -> string) ->
- ('a, 'b, 'c, 'd) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 0d47edbedc4..f5d4e2a837b 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -52,7 +52,6 @@ module D =
let rehash x = !rehash_ref x
let copy = Datatype.undefined
let pretty fmt p = Format.fprintf fmt "project %S" p.unique_name
- let varname p = "p_" ^ p.name
let mem_project f x = f x
end)
include (D: Datatype.S_no_copy with type t = Project_skeleton.t)
diff --git a/src/libraries/project/state.ml b/src/libraries/project/state.ml
index 0ad6eafe40d..11e05b3eefe 100644
--- a/src/libraries/project/state.ml
+++ b/src/libraries/project/state.ml
@@ -105,7 +105,7 @@ include Datatype.Make_with_collections
let copy = Datatype.undefined
let rehash = Datatype.undefined
let pretty fmt s = Format.fprintf fmt "state %S" s.unique_name
- let varname = Datatype.undefined
+
let mem_project = Datatype.never_any_project
end)
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index d1e5ef01cfc..332c480a667 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -681,7 +681,7 @@ struct
let copy = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
+
let mem_project = Datatype.never_any_project
end)
let () = Type.set_ml_name D.ty None
diff --git a/src/libraries/utils/rangemap.ml b/src/libraries/utils/rangemap.ml
index a6bd7aa4744..cd50b6aff9f 100644
--- a/src/libraries/utils/rangemap.ml
+++ b/src/libraries/utils/rangemap.ml
@@ -534,7 +534,7 @@ module Make(Ord: Datatype.S)(Value: Value) = struct
in aux
let pretty = Datatype.undefined
- let varname = Datatype.undefined
+
let mem_project =
if Ord.mem_project == Datatype.never_any_project &&
Value.mem_project == Datatype.never_any_project then
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index f0ec1a3c1b9..bafd391331d 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -46,7 +46,7 @@ module Aorai_state =
let compare x y = Datatype.Int.compare x.nums y.nums
let copy = Datatype.identity
let pretty fmt x = Format.fprintf fmt "state_%d" x.nums
- let varname _ = assert false
+
let mem_project = Datatype.never_any_project
end
)
@@ -66,7 +66,7 @@ module Aorai_typed_trans =
let compare x y = Datatype.Int.compare x.numt y.numt
let copy = Datatype.identity
let pretty = Promelaoutput.Typed.print_transition
- let varname _ = assert false
+
let mem_project = Datatype.never_any_project
end)
@@ -1821,7 +1821,7 @@ module Range = Datatype.Make_with_collections
Cil_datatype.Term.pretty c2
| Unbounded c1 -> Format.fprintf fmt "[%d..]" c1
| Unknown -> Format.fprintf fmt "[..]"
- let varname _ = "r"
+
let mem_project = Datatype.never_any_project
end)
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index 99645c1fefe..7d518f77bee 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -82,7 +82,7 @@ module Pred_or_term =
| PoT_pred p -> Printer.pp_predicate fmt p
| PoT_term t -> Printer.pp_term fmt t
- let varname _ = "pred_or_term"
+
end)
(** [Ext_logic_label] associates a statement to a label when necessary. For
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index c6902760336..92896d1c8af 100644
--- a/src/plugins/obfuscator/obfuscator_kind.ml
+++ b/src/plugins/obfuscator/obfuscator_kind.ml
@@ -85,7 +85,7 @@ include Datatype.Make_with_collections
let hash (k:k) = Hashtbl.hash k
let equal (k1:k) k2 = k1 = k2
let compare (k1:k) k2 = Stdlib.compare k1 k2
- let varname _ = "k"
+
let copy = Datatype.identity
let structural_descr = Structural_descr.t_abstract
let rehash = Datatype.identity
diff --git a/src/plugins/pdg_types/pdgTypes.ml b/src/plugins/pdg_types/pdgTypes.ml
index 89cbb18c701..3f215477f38 100644
--- a/src/plugins/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg_types/pdgTypes.ml
@@ -80,7 +80,7 @@ end
let pretty = print_id
let rehash = Datatype.identity
let copy = Datatype.undefined
- let varname = Datatype.undefined
+
let mem_project = Datatype.never_any_project
end)
: Datatype.S_with_collections with type t := t)
diff --git a/src/plugins/slicing/Slicing.mli b/src/plugins/slicing/Slicing.mli
old mode 100644
new mode 100755
diff --git a/src/plugins/slicing/slicingTypes.ml b/src/plugins/slicing/slicingTypes.ml
index 5391e63fc78..74a1954e156 100644
--- a/src/plugins/slicing/slicingTypes.ml
+++ b/src/plugins/slicing/slicingTypes.ml
@@ -65,7 +65,7 @@ module Fct_user_crit =
let reprs = [ SlicingInternals.dummy_fct_user_crit ]
let name = "SlicingTypes.Fct_user_crit"
let mem_project = Datatype.never_any_project
- let varname _ = "user_criteria"
+
end)
(** Function slice *)
@@ -88,7 +88,6 @@ module Sl_project =
type t = sl_project
let reprs = [ SlicingInternals.dummy_project ]
let name = "SlicingTypes.Sl_project"
- let varname _s = "sl_project_"
let mem_project = Datatype.never_any_project
end)
@@ -102,7 +101,6 @@ module Sl_select =
(fun v -> v, SlicingInternals.dummy_fct_user_crit)
Cil_datatype.Varinfo.reprs
let name = "SlicingTypes.Sl_select"
- let varname _s = "sl_select"
let mem_project = Datatype.never_any_project
end)
@@ -175,7 +173,7 @@ module Sl_mark =
let rehash = Datatype.undefined
let pretty = pp_sl_mark
let mem_project = Datatype.never_any_project
- let varname = Datatype.undefined
+
end)
let dyn_sl_mark = Sl_mark.ty
diff --git a/src/plugins/value/partitioning/split_strategy.ml b/src/plugins/value/partitioning/split_strategy.ml
index c99e49e1754..2bd967b0b95 100644
--- a/src/plugins/value/partitioning/split_strategy.ml
+++ b/src/plugins/value/partitioning/split_strategy.ml
@@ -64,7 +64,7 @@ include
| SplitEqList l ->
Format.fprintf fmt "Split on \\result == %a"
(Pretty_utils.pp_list ~sep:",@ " Datatype.Integer.pretty) l
- let varname _ = "v"
+
let mem_project = Datatype.never_any_project
end)
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index 4408fd24631..28b0cbfff37 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -375,7 +375,7 @@ module Datatype_Offsm_or_top = Datatype.Make_with_collections(struct
let pretty fmt = function
| Top -> Format.pp_print_string fmt "TopO"
| O o -> Format.fprintf fmt "O @[%a@]" V_Offsetmap.pretty o
- let varname _ = "o"
+
let mem_project = Datatype.never_any_project
end)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index e1fc93ee85a..3640e3bc0f5 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -857,7 +857,7 @@ module V_Or_Uninitialized = struct
let copy = Datatype.undefined
let rehash = Datatype.identity
let pretty = pretty
- let varname = Datatype.undefined
+
let mem_project = Datatype.never_any_project
end)
: Datatype.S with type t := t)
diff --git a/src/plugins/value_types/function_Froms.ml b/src/plugins/value_types/function_Froms.ml
index 00d0cfa6ad4..e894f38ca7b 100644
--- a/src/plugins/value_types/function_Froms.ml
+++ b/src/plugins/value_types/function_Froms.ml
@@ -57,7 +57,7 @@ struct
let rehash = Datatype.identity
let mem_project = Datatype.never_any_project
- let varname _ = "da"
+
let copy = Datatype.undefined
end)
@@ -177,7 +177,7 @@ module DepsOrUnassigned = struct
let rehash = Datatype.identity
let mem_project = Datatype.never_any_project
- let varname _ = "d"
+
let copy = Datatype.undefined
@@ -625,7 +625,7 @@ include Datatype.Make
let pretty = pretty
let rehash = Datatype.identity
let copy = Datatype.undefined
- let varname = Datatype.undefined
+
let mem_project = Datatype.never_any_project
end)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index bf35e910cd2..74b70f769ec 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -682,7 +682,7 @@ struct
let compare = Datatype.undefined
let hash = Datatype.undefined
let copy _old = QZERO.create ()
- let varname = Datatype.undefined
+
let pretty = Datatype.undefined
let mem_project _ _ = false
end)
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index befde666400..31e45621337 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -584,7 +584,7 @@ module C_object = Datatype.Make(struct
let mem_project = Datatype.Undefined.mem_project
- let varname _ = "co"
+
end)
let rec compare_ptr_conflated a b =
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index ec12ebe8695..0a6356d6aef 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -262,7 +262,7 @@ module PropIdRaw =
let rehash = Datatype.identity
let pretty = Datatype.undefined
let mem_project = Datatype.never_any_project
- let varname = Datatype.undefined
+
end)
(* -------------------------------------------------------------------------- *)
--
GitLab