[kernel] Remove deprecated module `LegacyNames`

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                                                     --- *)
 (* -------------------------------------------------------------------------- *)

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