From 03dee74a67fded628c79f2bac5641db525ee8435 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 10 Sep 2024 09:53:30 +0200
Subject: [PATCH] [kernel] Remove unused extension_from function
---
src/kernel_services/ast_queries/acsl_extension.ml | 5 +----
src/kernel_services/ast_queries/logic_env.ml | 6 +-----
src/kernel_services/ast_queries/logic_env.mli | 4 ----
3 files changed, 2 insertions(+), 13 deletions(-)
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 913ea0e95b..f5c221bc25 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/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
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 8dc8dae119..0f46da80c6 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/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
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index c82bcbe2a2..3f9907cc2d 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/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.
--
GitLab