diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 16f4828980bb0c648de24f4539b7978aa5735cfb..d45b91734daebbe69d4e15629b11c5587c0a25a1 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1065,210 +1065,6 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_string io_name
pp_other_loc io_loc
-(* -------------------------------------------------------------------------- *)
-(* --- Legacy Property Names --- *)
-(* -------------------------------------------------------------------------- *)
-
-(* Shall be deprecated *)
-module LegacyNames =
-struct
-
- module NamesTbl =
- State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
- (struct
- let name = "PropertyNames"
- let dependencies = [ ]
- let size = 97
- end)
- module IndexTbl =
- State_builder.Hashtbl(Hashtbl)(Datatype.String)
- (struct
- let name = "PropertyIndex"
- let dependencies = [ Ast.self; NamesTbl.self; Globals.Functions.self ]
- let size = 97
- end)
-
- let self = IndexTbl.self
-
- let kf_prefix kf = (Ast_info.Function.get_vi kf.fundec).vname ^ "_"
-
- let ident_names names =
- List.filter (function "" -> true
- | _ as n -> '\"' <> (String.get n 0) ) names
-
- let pp_names fmt l =
- let l = ident_names l in
- match l with [] -> ()
- | _ -> Format.fprintf fmt "_%a"
- (Pretty_utils.pp_list ~sep:"_" Format.pp_print_string) l
-
- let pp_code_annot_names fmt ca =
- match ca.annot_content with
- | AAssert(for_bhv,pred) | AInvariant(for_bhv,_,pred) ->
- let named_pred = pred.tp_statement in
- let pp_for_bhv fmt l =
- match l with
- | [] -> ()
- | _ -> Format.fprintf fmt "_for_%a"
- (Pretty_utils.pp_list ~sep:"_" Format.pp_print_string) l
- in
- Format.fprintf fmt "%a%a" pp_names named_pred.pred_name pp_for_bhv for_bhv
- | AVariant(term, _) -> pp_names fmt term.term_name
- | _ -> () (* TODO : add some more names ? *)
-
- let behavior_prefix b =
- if Cil.is_default_behavior b then ""
- else b.b_name ^ "_"
-
- let variant_suffix = function
- | (_,Some s) -> s.l_var_info.lv_name
- | _ -> ""
-
- let string_of_termination_kind = function
- Normal -> "post"
- | Exits -> "exit"
- | Breaks -> "break"
- | Continues -> "continue"
- | Returns -> "return"
-
- let stmt_prefix _s = "stmt_"
-
- let ki_prefix = function Kglobal -> "" | Kstmt s -> stmt_prefix s
-
- let extended_loc_prefix = function
- | ELContract kf -> kf_prefix kf
- | ELStmt (kf,s) -> kf_prefix kf ^ stmt_prefix s
- | ELGlob -> "global_"
-
- let other_loc_prefix = function
- | OLContract kf -> kf_prefix kf
- | OLStmt (kf,s) -> kf_prefix kf ^ stmt_prefix s
- | OLGlob _ -> "global_"
-
- let predicate_kind_txt pk ki =
- let name = match pk with
- | PKRequires b -> (behavior_prefix b) ^ "pre"
- | PKAssumes b -> (behavior_prefix b) ^ "assume"
- | PKEnsures (b, tk) -> (behavior_prefix b) ^ string_of_termination_kind tk
- | PKTerminates -> "term"
- in
- (ki_prefix ki) ^ name
-
- let active_prefix fmt a =
- let print_one a = Format.fprintf fmt "_%s" a in
- Datatype.String.Set.iter print_one a
-
- let rec id_prop_txt p = match p with
- | IPPredicate {ip_kind=pk;ip_kf=kf;ip_kinstr=ki;ip_pred=idp} ->
- Format.asprintf "%s%s%a"
- (kf_prefix kf) (predicate_kind_txt pk ki)
- pp_names (Logic_const.pred_of_id_pred idp).pred_name
- | IPExtended {ie_ext={ext_name};ie_loc=le} ->
- Format.asprintf "%sextended%a" (extended_loc_prefix le) pp_names [ext_name]
- | IPCodeAnnot {ica_kf=kf; ica_ca=ca} ->
- let name = match ca.annot_content with
- | AAssert (_, {tp_kind}) -> Cil_printer.string_of_assert tp_kind
- | AInvariant (_,loop,{tp_kind}) ->
- let kw = if loop then "invariant" else "loop_invariant" in
- Cil_printer.ident_of_predicate ~kw tp_kind
- | APragma _ -> "pragma"
- | AStmtSpec _ -> "contract"
- | AAssigns _ -> "assigns"
- | AVariant _ -> "variant"
- | AAllocation _ -> "allocates"
- | AExtended(_,_,{ext_name}) -> ext_name
- in Format.asprintf "%s%s%a" (kf_prefix kf) name pp_code_annot_names ca
- | IPComplete {ic_kf=kf; ic_kinstr=ki; ic_active=a; ic_bhvs=lb} ->
- let lb = Datatype.String.Set.elements lb in
- Format.asprintf "%s%s%acomplete%a"
- (kf_prefix kf) (ki_prefix ki) active_prefix a pp_names lb
- | IPDisjoint {ic_kf=kf; ic_kinstr=ki; ic_active=a; ic_bhvs=lb} ->
- let lb = Datatype.String.Set.elements lb in
- Format.asprintf "%s%s%adisjoint%a"
- (kf_prefix kf) (ki_prefix ki) active_prefix a pp_names lb
- | IPDecrease {id_kf=kf; id_ca=None; id_variant=variant} ->
- (kf_prefix kf) ^ "decr" ^ (variant_suffix variant)
- | IPDecrease {id_kf=kf; id_variant=variant} ->
- (kf_prefix kf) ^ "loop_term" ^ (variant_suffix variant)
- | IPAxiomatic {iax_name} -> "axiomatic_" ^ iax_name
- | IPLemma {il_name=name; il_pred} ->
- Format.asprintf "%s_%s%a"
- (Cil_printer.ident_of_lemma il_pred.tp_kind)
- name pp_names il_pred.tp_statement.pred_name
- | IPTypeInvariant {iti_name; iti_pred} ->
- Format.asprintf "type_invariant_%s%a"
- iti_name pp_names iti_pred.pred_name
- | IPGlobalInvariant {igi_name; igi_pred} ->
- Format.asprintf "global_invariant_%s%a"
- igi_name pp_names igi_pred.pred_name
- | IPAllocation {ial_kf=kf; ial_kinstr=ki; ial_bhv=Id_contract (a,b)} ->
- Format.asprintf "%s%s%a%sallocates"
- (kf_prefix kf) (ki_prefix ki) active_prefix a (behavior_prefix b)
- | IPAllocation {ial_kf=kf; ial_kinstr=Kstmt _; ial_bhv=Id_loop ca} ->
- Format.asprintf "%sloop_allocates%a"
- (kf_prefix kf) pp_code_annot_names ca
- | IPAllocation _ -> assert false
- | IPAssigns {ias_kf=kf; ias_kinstr=ki; ias_bhv=Id_contract (a,b)} ->
- Format.asprintf "%s%s%a%sassign"
- (kf_prefix kf) (ki_prefix ki) active_prefix a (behavior_prefix b)
- | IPAssigns {ias_kf=kf; ias_kinstr=Kstmt _; ias_bhv=Id_loop ca} ->
- Format.asprintf "%sloop_assign%a"
- (kf_prefix kf) pp_code_annot_names ca
- | IPAssigns _ -> assert false
- | IPFrom {if_from=(out,_)} ->
- "from_id_"^(string_of_int (out.it_id))
- | IPReachable _ -> "reachable_stmt"
- | IPBehavior {ib_kf=kf; ib_kinstr=ki; ib_active=a; ib_bhv=b} ->
- Format.asprintf "%s%s%a%s"
- (kf_prefix kf) (ki_prefix ki) active_prefix a b.b_name
- | IPPropertyInstance {ii_kf=kf; ii_stmt=stmt; ii_ip=ip} ->
- Format.asprintf "specialization_%s_at_%t" (id_prop_txt ip)
- (fun fmt ->
- Format.fprintf fmt "%a_stmt_%d" Kernel_function.pretty kf stmt.sid)
- | IPOther {io_name; io_loc} -> other_loc_prefix io_loc ^ io_name
-
- (** function used to normalize basename *)
- let normalize_basename s =
- let is_valid_char_id = function
- | 'a'..'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> true
- | _ -> false
- and is_numeric = function
- | '0'..'9' -> true
- | _ -> false
- in
- if s ="" then "property"
- else
- let s = String.map (fun c -> if not (is_valid_char_id c) then '_' else c) s in
- if is_numeric s.[0] then "property_" ^ s else s
-
- (** returns the name that should be returned by the function [get_prop_name_id] if the given property has [name] as basename. That name is reserved so that [get_prop_name_id prop] can never return an identical name. *)
- let reserve_name_id basename =
- let basename = normalize_basename basename in
- try
- let speed_up_start = NamesTbl.find basename in
- (* this basename is already reserved *)
- let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
- in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
- unique_name
- with Not_found -> (* first time that basename is reserved *)
- NamesTbl.add basename 2 ;
- basename
-
- (** returns the basename of the property. *)
- let get_prop_basename ip = normalize_basename (id_prop_txt ip)
-
- (** returns a unique name identifying the property.
- This name is built from the basename of the property. *)
- let get_prop_name_id ip =
- try IndexTbl.find ip
- with Not_found -> (* first time we are asking for a name for that [ip] *)
- let basename = get_prop_basename ip in
- let unique_name = reserve_name_id basename in
- IndexTbl.add ip unique_name ;
- unique_name
-
-end
-
(* -------------------------------------------------------------------------- *)
(* --- Property Names --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 6d9f38b4c4eb2f6c042f597bdbeeab29ebbf9a24..eaf6c8bc0db251ebc066d74efacee36d742d1a6b 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -519,16 +519,6 @@ val source: identified_property -> Filepath.position option
(** {2 names} *)
(**************************************************************************)
-
-(** @since 19.0-Potassium deprecated old naming scheme,
- to be removed in future versions. *)
-module LegacyNames :
-sig
- val self: State.t
- val get_prop_basename: identified_property -> string
- val get_prop_name_id: identified_property -> string
-end
-
(** @since Oxygen-20120901 *)
module Names :
sig