[kernel] Remove unused extension_from function

src/kernel_services/ast_queries/acsl_extension.ml

@@ -320,8 +320,6 @@ module Extensions = struct
   let is_same_ext ~plugin name ext1 ext2 =
     let is_same = (find_common ~plugin name).is_same_ext in
     is_same ext1 ext2
-
-  let extension_from name = (find_common ~plugin:None name).plugin
 end
 
 (* Registration functions *)
@@ -351,8 +349,7 @@ let () =
     ~is_extension: Extensions.is_extension
     ~preprocess: Extensions.preprocess
     ~is_extension_block: Extensions.is_extension_block
-    ~preprocess_block: Extensions.preprocess_block
-    ~extension_from:Extensions.extension_from;
+    ~preprocess_block: Extensions.preprocess_block;
   Logic_typing.set_extension_handler
     ~is_extension: Extensions.is_extension
     ~typer: Extensions.typing

src/kernel_services/ast_queries/logic_env.ml

@@ -31,17 +31,15 @@ module Extensions = struct
   let ref_preprocess = ref (fun ~plugin:_ _ -> assert false)
   let ref_is_extension_block = ref (fun ~plugin:_ _ -> assert false)
   let ref_preprocess_block = ref (fun ~plugin:_ _ -> assert false)
-  let ref_extension_from = ref (fun _ -> assert false)
 
   let set_extension_handler ~category ~is_extension ~preprocess
-      ~is_extension_block ~preprocess_block ~extension_from =
+      ~is_extension_block ~preprocess_block =
     assert (not !initialized) ;
     ref_is_extension := is_extension ;
     ref_category := category ;
     ref_preprocess := preprocess ;
     ref_is_extension_block := is_extension_block;
     ref_preprocess_block := preprocess_block;
-    ref_extension_from := extension_from;
     initialized := true ;
     ()
 
@@ -50,7 +48,6 @@ module Extensions = struct
   let category ~plugin name = !ref_category ~plugin name
   let preprocess ~plugin name = !ref_preprocess ~plugin name
   let preprocess_block ~plugin name = !ref_preprocess_block ~plugin name
-  let extension_from name = !ref_extension_from name
 end
 let set_extension_handler = Extensions.set_extension_handler
 let is_extension = Extensions.is_extension
@@ -58,7 +55,6 @@ let is_extension_block = Extensions.is_extension_block
 let extension_category = Extensions.category
 let preprocess_extension = Extensions.preprocess
 let preprocess_extension_block = Extensions.preprocess_block
-let extension_from = Extensions.extension_from
 
 let error (b,_e) fstring =
   Kernel.abort

src/kernel_services/ast_queries/logic_env.mli

@@ -62,9 +62,6 @@ val preprocess_extension_block:
   plugin:string option -> string -> string * Logic_ptree.extended_decl list ->
   string * Logic_ptree.extended_decl list
 
-(** Return the plugin name of the extension. *)
-val extension_from : string -> string
-
 (** {2 Global Tables} *)
 module Logic_info: State_builder.Hashtbl
   with type key = string and type data = Cil_types.logic_info list
@@ -255,7 +252,6 @@ val set_extension_handler:
   preprocess_block:
     (plugin:string option -> string -> string * Logic_ptree.extended_decl list ->
      string * Logic_ptree.extended_decl list) ->
-  extension_from:(string -> string) ->
   unit
 (** Used to setup references related to the handling of ACSL extensions.
     If your name is not [Acsl_extension], do not call this.